--- a/src/HOL/Tools/inductive_realizer.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Apr 26 22:38:05 2006 +0200
@@ -208,7 +208,7 @@
else NONE) rss;
val fs = List.concat (snd (foldl_map (fn (intrs, (prems, dummy)) =>
let
- val (intrs1, intrs2) = splitAt (length prems, intrs);
+ val (intrs1, intrs2) = chop (length prems) intrs;
val fs = map (fn (rule, intr) =>
fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1)
in (intrs2, if dummy then Const ("arbitrary",
@@ -330,7 +330,7 @@
if s mem rsets then
let
val (d :: dummies') = dummies;
- val (recs1, recs2) = splitAt (length rs, if d then tl recs else recs)
+ val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
end
--- a/src/HOL/Tools/typedef_package.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/HOL/Tools/typedef_package.ML Wed Apr 26 22:38:05 2006 +0200
@@ -119,11 +119,11 @@
fun mk_nonempty A =
HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
val goal = mk_nonempty set;
- val goal_pat = mk_nonempty (Var (if_none (Syntax.read_variable name) (name, 0), setT));
+ val goal_pat = mk_nonempty (Var (the_default (name, 0) (Syntax.read_variable name), setT));
(*lhs*)
val defS = Sign.defaultS thy;
- val lhs_tfrees = map (fn v => (v, if_none (AList.lookup (op =) rhs_tfrees v) defS)) vs;
+ val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
val args_setT = lhs_tfrees
|> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
|> map TFree;
@@ -132,7 +132,7 @@
val full_tname = full tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
- val (Rep_name, Abs_name) = if_none opt_morphs ("Rep_" ^ name, "Abs_" ^ name);
+ val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
val setT' = map Term.itselfT args_setT ---> setT;
val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
val RepC = Const (full Rep_name, newT --> oldT);
@@ -303,7 +303,7 @@
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
- typedef ((def, if_none opt_name (Syntax.type_name t mx)), (t, vs, mx), A, morphs);
+ typedef ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
val typedefP =
OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
--- a/src/Provers/eqsubst.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Provers/eqsubst.ML Wed Apr 26 22:38:05 2006 +0200
@@ -61,9 +61,8 @@
in
(case t' of
(_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
- Seq.cons(f ft,
- maux (IsaFTerm.focus_right ft)))
- | (Abs _) => Seq.cons(f ft, maux (IsaFTerm.focus_abs ft))
+ Seq.cons (f ft) (maux (IsaFTerm.focus_right ft)))
+ | (Abs _) => Seq.cons (f ft) (maux (IsaFTerm.focus_abs ft))
| leaf => Seq.single (f ft)) end
in maux ft end;
@@ -76,10 +75,9 @@
in
(case (IsaFTerm.focus_of_fcterm ft) of
(_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
- Seq.cons(hereseq,
- maux (IsaFTerm.focus_right ft)))
- | (Abs _) => Seq.cons(hereseq, maux (IsaFTerm.focus_abs ft))
- | leaf => Seq.single (hereseq))
+ Seq.cons hereseq (maux (IsaFTerm.focus_right ft)))
+ | (Abs _) => Seq.cons hereseq (maux (IsaFTerm.focus_abs ft))
+ | leaf => Seq.single hereseq)
end
in maux ft end;
--- a/src/Pure/General/file.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/General/file.ML Wed Apr 26 22:38:05 2006 +0200
@@ -103,7 +103,7 @@
fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
fun is_dir path =
- if_none (try OS.FileSys.isDir (platform_path path)) false;
+ the_default false (try OS.FileSys.isDir (platform_path path));
(* read / write files *)
--- a/src/Pure/General/scan.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/General/scan.ML Wed Apr 26 22:38:05 2006 +0200
@@ -248,7 +248,7 @@
fun drain def_prmpt get stopper scan ((state, xs), src) =
(scan (state, xs), src) handle MORE prmpt =>
- (case get (if_none prmpt def_prmpt) src of
+ (case get (the_default def_prmpt prmpt) src of
([], _) => (finite' stopper scan (state, xs), src)
| (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src'));
@@ -258,7 +258,7 @@
fun drain_loop recover inp =
drain_with (catch scanner) inp handle FAIL msg =>
- (Output.error_msg (if_none msg "Syntax error."); drain_with recover inp);
+ (Output.error_msg (the_default "Syntax error." msg); drain_with recover inp);
val ((ys, (state', xs')), src') =
(case (get def_prmpt src, opt_recover) of
--- a/src/Pure/General/symbol.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/General/symbol.ML Wed Apr 26 22:38:05 2006 +0200
@@ -499,7 +499,7 @@
else if s = "\\<spacespace>" then 2
else 1;
-fun sym_length ss = Library.foldl (fn (n, s) => sym_len s + n) (0, ss);
+fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
fun symbol_output str =
if chars_only str then default_output str
--- a/src/Pure/Isar/attrib.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Isar/attrib.ML Wed Apr 26 22:38:05 2006 +0200
@@ -219,7 +219,7 @@
fun the_type types xi = the (types xi)
handle Option.Option => error_var "No such variable in theorem: " xi;
-fun unify_types thy types ((unifier, maxidx), (xi, u)) =
+fun unify_types thy types (xi, u) (unifier, maxidx) =
let
val T = the_type types xi;
val U = Term.fastype_of u;
@@ -283,7 +283,7 @@
val types' = #1 (Drule.types_sorts thm');
val unifier = map (apsnd snd) (Vartab.dest (#1
- (Library.foldl (unify_types thy types') ((Vartab.empty, 0), internal_insts))));
+ (fold (unify_types thy types') internal_insts (Vartab.empty, 0))));
val type_insts'' = map (typ_subst unifier) type_insts';
val internal_insts'' = map (subst unifier) internal_insts;
--- a/src/Pure/Isar/context_rules.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Isar/context_rules.ML Wed Apr 26 22:38:05 2006 +0200
@@ -108,9 +108,9 @@
val rules = Library.merge (fn ((_, (k1, th1)), (_, (k2, th2))) =>
k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) (rules1, rules2);
val next = ~ (length rules);
- val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) =>
- nth_map i (curry insert_tagged_brl ((w, n), (b, th))) nps)
- (empty_netpairs, next upto ~1 ~~ rules);
+ val netpairs = fold (fn (n, (w, ((i, b), th))) =>
+ nth_map i (curry insert_tagged_brl ((w, n), (b, th))))
+ (next upto ~1 ~~ rules) empty_netpairs;
in make_rules (next - 1) rules netpairs wrappers end
fun print generic (Rules {rules, ...}) =
--- a/src/Pure/Proof/proof_rewrite_rules.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Wed Apr 26 22:38:05 2006 +0200
@@ -200,7 +200,7 @@
fun strip [] t = t
| strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
in
- strip Ts (Library.foldl (uncurry lambda o Library.swap) (t', frees))
+ strip Ts (fold lambda frees t')
end;
fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
--- a/src/Pure/Proof/proof_syntax.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Wed Apr 26 22:38:05 2006 +0200
@@ -97,7 +97,7 @@
val thms' = map (apsnd Thm.full_prop_of) (PureThy.all_thms_of thy);
val tab = Symtab.foldl (fn (tab, (key, ps)) =>
- let val prop = if_none (AList.lookup (op =) thms' key) (Bound 0)
+ let val prop = the_default (Bound 0) (AList.lookup (op =) thms' key)
in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
if prop <> prop' then
(Symtab.update (key ^ "_" ^ string_of_int i, prf) tab, i+1)
@@ -110,7 +110,7 @@
| rename (prf % t) = rename prf % t
| rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
let
- val prop' = if_none (AList.lookup (op =) thms' s) (Bound 0);
+ val prop' = the_default (Bound 0) (AList.lookup (op =) thms' s);
val ps = remove (op =) prop' (map fst (the (Symtab.lookup thms s)))
in if prop = prop' then prf' else
PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
@@ -180,16 +180,16 @@
val Oraclet = Const ("Oracle", propT --> proofT);
val MinProoft = Const ("MinProof", proofT);
-val mk_tyapp = Library.foldl (fn (prf, T) => Const ("Appt",
+val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
[proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
fun term_of _ (PThm ((name, _), _, _, NONE)) =
Const (NameSpace.append "thm" name, proofT)
| term_of _ (PThm ((name, _), _, _, SOME Ts)) =
- mk_tyapp (Const (NameSpace.append "thm" name, proofT), Ts)
+ mk_tyapp Ts (Const (NameSpace.append "thm" name, proofT))
| term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT)
| term_of _ (PAxm (name, _, SOME Ts)) =
- mk_tyapp (Const (NameSpace.append "axm" name, proofT), Ts)
+ mk_tyapp Ts (Const (NameSpace.append "axm" name, proofT))
| term_of _ (PBound i) = Bound i
| term_of Ts (Abst (s, opT, prf)) =
let val T = the_default dummyT opT
--- a/src/Pure/Proof/reconstruct.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Proof/reconstruct.ML Wed Apr 26 22:38:05 2006 +0200
@@ -57,7 +57,7 @@
(Envir.Envir {iTs = iTs, asol = asol, maxidx = maxidx+1},
TVar (("'t", maxidx+1), s));
-fun mk_abs Ts t = Library.foldl (fn (u, T) => Abs ("", T, u)) (t, Ts);
+val mk_abs = fold (fn T => fn u => Abs ("", T, u));
fun unifyT sg env T U =
let
--- a/src/Pure/Syntax/ast.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Syntax/ast.ML Wed Apr 26 22:38:05 2006 +0200
@@ -129,7 +129,7 @@
| fold_ast _ [y] = y
| fold_ast c (x :: xs) = Appl [Constant c, x, fold_ast c xs];
-fun fold_ast_p c = Library.foldr (fn (x, xs) => Appl [Constant c, x, xs]);
+fun fold_ast_p c = uncurry (fold_rev (fn x => fn xs => Appl [Constant c, x, xs]));
(* unfold asts *)
--- a/src/Pure/Syntax/syn_trans.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Wed Apr 26 22:38:05 2006 +0200
@@ -276,7 +276,7 @@
fun abs_tr' tm =
- Library.foldr (fn (x, t) => Lexicon.const "_abs" $ x $ t)
+ uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
(strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
fun atomic_abs_tr' (x, T, t) =
--- a/src/Pure/Thy/thy_info.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Apr 26 22:38:05 2006 +0200
@@ -86,7 +86,7 @@
handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
fun upd_deps name entry G =
- Library.foldl (fn (H, parent) => Graph.del_edge (parent, name) H) (G, Graph.imm_preds G name)
+ fold (fn parent => Graph.del_edge (parent, name)) (Graph.imm_preds G name) G
|> Graph.map_node name (K entry);
fun update_node name parents entry G =
@@ -243,8 +243,8 @@
(* load_file *)
val opt_path = Option.map (Path.dir o fst o ThyLoad.get_thy);
-fun opt_path' (d: deps option) = if_none (Option.map (opt_path o #master) d) NONE;
-fun opt_path'' d = if_none (Option.map opt_path' d) NONE;
+fun opt_path' (d: deps option) = the_default NONE (Option.map (opt_path o #master) d);
+fun opt_path'' d = the_default NONE (Option.map opt_path' d);
local
@@ -360,7 +360,7 @@
handle ERROR msg => cat_error msg
(loader_msg "the error(s) above occurred while examining theory" [name] ^
(if null initiators then "" else required_by "\n" initiators));
- val dir' = if_none (opt_path'' new_deps) dir;
+ val dir' = the_default dir (opt_path'' new_deps);
val (visited', parent_results) = foldl_map (req_parent dir') (name :: visited, parents);
val thy = if not really then SOME (get_theory name) else NONE;
@@ -424,7 +424,7 @@
let
val bparents = map base_of_path parents;
val dir' = opt_path'' (lookup_deps name);
- val dir = if_none dir' Path.current;
+ val dir = the_default Path.current dir';
val assert_thy = if int then quiet_update_thy' true dir else weak_use_thy dir;
val _ = check_unfinished error name;
val _ = List.app assert_thy parents;
--- a/src/Pure/codegen.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/codegen.ML Wed Apr 26 22:38:05 2006 +0200
@@ -516,12 +516,12 @@
fun theory_of_type s thy =
if Sign.declared_tyname thy s
- then SOME (if_none (get_first (theory_of_type s) (Theory.parents_of thy)) thy)
+ then SOME (the_default thy (get_first (theory_of_type s) (Theory.parents_of thy)))
else NONE;
fun theory_of_const s thy =
if Sign.declared_const thy s
- then SOME (if_none (get_first (theory_of_const s) (Theory.parents_of thy)) thy)
+ then SOME (the_default thy (get_first (theory_of_const s) (Theory.parents_of thy)))
else NONE;
fun thyname_of_type s thy = (case theory_of_type s thy of
@@ -587,7 +587,7 @@
NONE => defs
| SOME (s, (T, (args, rhs))) => Symtab.update
(s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) ::
- if_none (Symtab.lookup defs s) []) defs))
+ the_default [] (Symtab.lookup defs s)) defs))
in
foldl (fn ((thyname, axms), defs) =>
Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss
--- a/src/Pure/proof_general.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/proof_general.ML Wed Apr 26 22:38:05 2006 +0200
@@ -172,12 +172,12 @@
("class", pgip_class),
("seq", string_of_int (pgip_serial())),
("id", !pgip_id)] @
- if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
+ the_default [] (Option.map (single o (pair "destid")) (! pgip_refid)) @
(* destid=refid since Isabelle only communicates back to sender,
so we may omit refid from attributes.
- if_none (Option.map (single o (pair "refid")) (! pgip_refid)) [] @
+ the_default [] (Option.map (single o (pair "refid")) (! pgip_refid)) @
*)
- if_none (Option.map (single o (pair "refseq")) (! pgip_refseq)) [])
+ the_default [] (Option.map (single o (pair "refseq")) (! pgip_refseq)))
pgips;
in
@@ -1102,7 +1102,7 @@
("default", default)]
[ty]) prefs)]) (!preferences)
-fun allprefs () = Library.foldl (op @) ([], map snd (!preferences))
+fun allprefs () = maps snd (!preferences)
fun setpref name value =
(case AList.lookup (op =) (allprefs ()) name of
--- a/src/Pure/pure_thy.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/pure_thy.ML Wed Apr 26 22:38:05 2006 +0200
@@ -415,8 +415,8 @@
fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
| smart_store name_thm (name, thms) =
let
- fun merge (thy, th) = Theory.merge (thy, Thm.theory_of_thm th);
- val thy = Library.foldl merge (Thm.theory_of_thm (hd thms), tl thms);
+ fun merge th thy = Theory.merge (thy, Thm.theory_of_thm th);
+ val thy = fold merge (tl thms) (Thm.theory_of_thm (hd thms));
in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
in
--- a/src/Pure/tactic.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/tactic.ML Wed Apr 26 22:38:05 2006 +0200
@@ -577,7 +577,7 @@
val rev_defs = sort_lhs_depths o map symmetric;
-fun fold_rule defs thm = Library.foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
+fun fold_rule defs = fold rewrite_rule (rev_defs defs);
fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
@@ -628,12 +628,12 @@
fun filter_prems_tac p =
let fun Then NONE tac = SOME tac
| Then (SOME tac) tac' = SOME(tac THEN' tac');
- fun thins ((tac,n),H) =
+ fun thins H (tac,n) =
if p H then (tac,n+1)
else (Then tac (rotate_tac n THEN' etac thin_rl),0);
in SUBGOAL(fn (subg,n) =>
let val Hs = Logic.strip_assums_hyp subg
- in case fst(Library.foldl thins ((NONE,0),Hs)) of
+ in case fst(fold thins Hs (NONE,0)) of
NONE => no_tac | SOME tac => tac n
end)
end;
--- a/src/Pure/term.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/term.ML Wed Apr 26 22:38:05 2006 +0200
@@ -390,7 +390,7 @@
in arg 0 [] tm end;
-val list_abs = Library.foldr (fn ((x, T), t) => Abs (x, T, t));
+val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));
fun strip_abs (Abs (a, T, t)) =
let val (a', t') = strip_abs t
--- a/src/Pure/unify.ML Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/unify.ML Wed Apr 26 22:38:05 2006 +0200
@@ -325,7 +325,7 @@
(mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
(env, dpairs)));
(*Produce sequence of all possible ways of copying the arg list*)
- fun copyargs [] = Seq.cons( ([],ed), Seq.empty)
+ fun copyargs [] = Seq.cons ([],ed) Seq.empty
| copyargs (uarg::uargs) = Seq.maps (copycons uarg) (copyargs uargs);
val (uhead,uargs) = strip_comb u;
val base = body_type env (fastype env (rbinder,uhead));
@@ -577,7 +577,7 @@
in add_unify 1 ((env, dps), Seq.empty) end;
fun unifiers (params as (thy, env, tus)) =
- Seq.cons ((fold (Pattern.unify thy) tus env, []), Seq.empty)
+ Seq.cons (fold (Pattern.unify thy) tus env, []) Seq.empty
handle Pattern.Unif => Seq.empty
| Pattern.Pattern => hounifiers params;