Lines Matching refs:fn
168 (fn (arg, x) => (Token.assign NONE arg; x));
170 fun unparse_kind k = Parse.group (fn () => Token.str_of_kind k)
173 val not_command = Parse.group (fn () => "non-command token")
175 fun command s = Parse.group (fn () => "command "^s)
176 (token (fn t => Token.is_command t andalso
208 >> (fn (left, (arr, right)) => arr (left, right)) end;
224 val mk_thy_body = List.map (fn (s,p) => Parse.command_name s |-- p);
234 (fn (x,(l1,l2)) => if (p x) then ([],(x::l1)::l2)
236 fun proof_qed i = Parse.group (fn () => "proof_qed")
237 (fn t =>
322 >> (fn ((x, y), z) => ((x, z), y)))
489 (fn ((a, b), c) => (a, (b, c)))
506 >> (fn t => (true, NONE, t))
507 || Parse.typ >> (fn t => (false, NONE, t))
521 fun unparse_cmd s = Parse.group (fn () => s)
522 (fn toks =>
546 first' (List.map (fn s => unparse_cmd s >>
548 first' (List.map (fn s => unparse_cmd s >>
687 val dbg = List.map (fn t => (Token.kind_of t,Token.content_of t));
691 #> (fn (((h,a),b),_) => Thy {header=h,args=a,body=b}));
781 = case get_first (fn f => SOME (f v)
791 = variant vname (K "") [fn SOME v' => attr name f v',
792 fn NONE => []];
806 (fn T' => if length (Thy_Info.loaded_files
817 [fn (s,SOME ((s1,[]),[])) => a "name" ("\""^s^"\" :: "^s1),
818 fn (s,NONE) => a "name" s] #> xml' "Keyword" [];
820 (Path.print #> b ? (fn s => "("^s^")")) p) [];
822 [fn ((name,_),(("",false),Expression.Named [])) =>
857 fn Parser.Arg i =>
859 fn Parser.TypArg i =>
861 fn Parser.String (_,s) =>
863 fn Parser.Break i =>
865 fn Parser.Block (i,symbs) =>
870 [fn Mixfix.NoSyn => NONE,
871 fn mx => Parser.format_const_mixfix state name mx tp
875 [fn Mixfix.NoSyn => NONE,
876 fn mx => Parser.format_type_mixfix name mx num_args
898 [fn Element.Fixes fixes => List.map (fn (b,_,mx) =>
905 fn Element.Assumes ass => List.map (fn (b,tms) =>
907 PolyML.makestring [fn [(tm,[])] =>
926 val get_tms = (fn (lhs,rhs) => (strip_cfun lhs,rhs)) o
930 val tms = map ((fn x => (get_imps x,get_tms x)) o
933 val fn_eqs = List.foldl (fn (eq,t) =>
944 val fns = List.foldl (fn (((b,_),mx),t) =>
947 in Symtab.fold_rev (fn (k,(tp,equations)) =>
950 val equations' = List.map (fn (b,imps,vs,tm) =>
961 in fn l => elem::l end) fn_eqs [] end end;
963 let val eqs' = List.map (fn ((b,l),tm) =>
970 HOLogic.dest_eq |> (fn (head,body) =>
972 val fn_eqs = List.foldl (fn (eq,t) =>
983 val fns = List.foldl (fn ((b,_,mx),t) =>
986 in Symtab.fold_rev (fn (k,(tp,equations)) =>
989 val equations' = List.map (fn (vs,tm) =>
996 in fn l => elem::l end) fn_eqs []
1000 [fn Element.Shows s => List.map (fn (b,tms) =>
1005 (List.map (fn (t,ts) => xml "Show" [] (
1022 (List.map (fn n => xml "class" (a "name" n) []) s)
1027 fn Defs ((unchecked,overloaded),l) =>
1028 let val l' = List.map (fn ((name,tm),args) =>
1043 fn Typedef (((((vars,tp),mx),tm),morphisms),proof) =>
1044 let val vars' = List.map (fn (name,sort) => case sort of
1062 fn Instantiation (arity,body) =>
1074 fn Instance (head,proof) =>
1082 val vars = xml "Vars" [] (List.map (fn s =>
1093 fn Subclass (target,cls,proof) =>
1100 fn Locale ((name,(parents,ctxt)),body) =>
1108 [fn (ps,[]) => List.map xml_of_expr ps] parents
1115 fn Class ((name,(parents,ctxt)),body) =>
1132 fn TypeSynonym (((target,vars),name),(typ,mx))
1142 (fn s => TFree (s,[]) |> XML_Syntax.xml_of_type)
1146 fn Datatype dts =>
1149 (fn ((name,vars,mx),cs) => xml "Datatype"
1153 List.map (fn (c,tms,mx) =>
1159 List.map (fn (v,s) =>
1173 @(List.map (fn (v,s) =>
1179 fn Consts cs => (xml "Consts" [] (List.map
1180 (fn (name,tp,mx) =>
1187 fn Axioms axs => (xml "Axioms" [] (List.map
1188 (fn (b,tm) => xml "Axiom"
1192 fn Lemma ((((target,(name,args)), strs),(ctxt,stmt)),proof) =>
1204 fn Definition (target,(name,(binding,tm))) =>
1216 (fn t => (HOLogic.dest_eq t
1218 |> (fn (head,body) =>
1229 fn Fun (target,((cfg,f),a)) =>
1234 fn Primrec ((target,f),a) =>
1238 fn Fixrec (target,(f,a)) =>
1242 fn Domain (unsafe,dts) =>
1244 val dts' = List.map (fn (((vs,name),mx), cs) =>
1245 let val vars = List.map (fn (a,s) =>
1251 val cs' = List.map (fn ((c,args),mx1) =>
1258 (List.map (fn (l,sel,tp) =>
1284 val thys = map (fn (i,_) => (Thy_Info.get_theory i; [])