Lines Matching refs:args
182 |-- Thy_Header.args);
641 args:(Token.T list * Thy_Header.header),
675 args:(Token.T list * Thy_Header.header),
691 #> (fn (((h,a),b),_) => Thy {header=h,args=a,body=b}));
851 fun attrs_of_binding state (name,args) =
853 attr "args" (List.map (Args.pretty_src (
855 #> space_implode ", ") args;
1028 let val l' = List.map (fn ((name,tm),args) =>
1033 val args' = List.map (Args.pretty_src
1035 args |> space_implode " "
1036 in xml "Def" (a "args" args'@attr_of_binding name@
1063 let val ([name],args',sort) = Class.read_multi_arity
1065 val args = List.map #2 args'
1072 ([xml_of_arity (args,sort)]@
1078 let val (names,args',sort) =
1081 val args = List.map #2 args'
1086 ([vars,xml_of_arity (args,sort)]))
1192 fn Lemma ((((target,(name,args)), strs),(ctxt,stmt)),proof) =>
1193 let val result = case (args,strs) of
1202 (args,strs))
1251 val cs' = List.map (fn ((c,args),mx1) =>
1266 args) end) cs
1281 val (Thy {header,args=(th,h),body}) =