--- a/src/HOL/Library/EfficientNat.thy Fri Jul 15 15:44:11 2005 +0200
+++ b/src/HOL/Library/EfficientNat.thy Fri Jul 15 15:44:15 2005 +0200
@@ -110,10 +110,10 @@
fun remove_suc thy thms =
let
val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
- val ctzero = cterm_of (sign_of Main.thy) HOLogic.zero;
+ val ctzero = cterm_of Main.thy HOLogic.zero;
val vname = variant (map fst
- (Library.foldl add_term_varnames ([], map prop_of thms))) "x";
- val cv = cterm_of (sign_of Main.thy) (Var ((vname, 0), HOLogic.natT));
+ (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
+ val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT));
fun lhs_of th = snd (Thm.dest_comb
(fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
@@ -172,7 +172,7 @@
let
val Suc_clause' = Thm.transfer thy Suc_clause;
val vname = variant (map fst
- (Library.foldl add_term_varnames ([], map prop_of thms))) "x";
+ (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
| find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
| find_var _ = NONE;
@@ -184,7 +184,7 @@
NONE => thms
| SOME ((th, th'), (Sucv, v)) =>
let
- val cert = cterm_of (sign_of_thm th);
+ val cert = cterm_of (Thm.theory_of_thm th);
val th'' = ObjectLogic.rulify (Thm.implies_elim
(Drule.fconv_rule (Thm.beta_conversion true)
(Drule.instantiate' []
--- a/src/HOL/Orderings.thy Fri Jul 15 15:44:11 2005 +0200
+++ b/src/HOL/Orderings.thy Fri Jul 15 15:44:15 2005 +0200
@@ -545,7 +545,7 @@
print_translation {*
let
fun mk v v' q n P =
- if v=v' andalso not(v mem (map fst (Term.add_frees([],n))))
+ if v=v' andalso not (v mem (map fst (Term.add_frees n [])))
then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match;
fun all_tr' [Const ("_bound",_) $ Free (v,_),
Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
--- a/src/HOL/Tools/inductive_codegen.ML Fri Jul 15 15:44:11 2005 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Jul 15 15:44:15 2005 +0200
@@ -180,8 +180,8 @@
val terms_vs = distinct o List.concat o (map term_vs);
(** collect all Vars in a term (with duplicates!) **)
-fun term_vTs t = map (apfst fst o dest_Var)
- (List.filter is_Var (foldl_aterms (op :: o Library.swap) ([], t)));
+fun term_vTs tm =
+ fold_aterms (fn Var ((x, _), T) => cons (x, T) | _ => I) tm [];
fun get_args _ _ [] = ([], [])
| get_args is i (x::xs) = (if i mem is then apfst else apsnd) (cons x)
--- a/src/HOL/Tools/inductive_package.ML Fri Jul 15 15:44:11 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML Fri Jul 15 15:44:15 2005 +0200
@@ -178,15 +178,14 @@
fun unify_consts thy cs intr_ts =
(let
val tsig = Sign.tsig_of thy;
- val add_term_consts_2 =
- foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
+ val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
fun varify (t, (i, ts)) =
let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
in (maxidx_of_term t', t'::ts) end;
val (i, cs') = foldr varify (~1, []) cs;
val (i', intr_ts') = foldr varify (i, []) intr_ts;
- val rec_consts = Library.foldl add_term_consts_2 ([], cs');
- val intr_consts = Library.foldl add_term_consts_2 ([], intr_ts');
+ val rec_consts = fold add_term_consts_2 cs' [];
+ val intr_consts = fold add_term_consts_2 intr_ts' [];
fun unify (env, (cname, cT)) =
let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
in Library.foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))
--- a/src/HOL/Tools/inductive_realizer.ML Fri Jul 15 15:44:11 2005 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Jul 15 15:44:15 2005 +0200
@@ -60,7 +60,7 @@
val params = map dest_Var ts;
val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr),
- map (Type.unvarifyT o snd) (rev (Term.add_vars ([], prop_of intr)) \\ params) @
+ map (Type.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
filter_out (equal Extraction.nullT) (map
(Type.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
NoSyn);
@@ -137,7 +137,7 @@
val args = map (Free o apfst fst o dest_Var)
(add_term_vars (prop_of intr, []) \\ map Var params);
val args' = map (Free o apfst fst)
- (Term.add_vars ([], prop_of intr) \\ params);
+ (Term.add_vars (prop_of intr) [] \\ params);
val rule' = strip_all rule;
val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
val used = map (fst o dest_Free) args;
@@ -213,7 +213,7 @@
HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
else fs)
end) (intrs, (premss ~~ dummies))));
- val frees = Library.foldl Term.add_frees ([], fs);
+ val frees = fold Term.add_frees fs [];
val Ts = map fastype_of fs;
val rlzs = List.mapPartial (fn (a, concl) =>
let val T = Extraction.etype_of thy vs [] concl
@@ -250,9 +250,9 @@
let
val prems = prems_of rule ~~ prems_of rrule;
val rvs = map fst (relevant_vars (prop_of rule));
- val xs = rev (Term.add_vars ([], prop_of rule));
+ val xs = rev (Term.add_vars (prop_of rule) []);
val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
- val rlzvs = rev (Term.add_vars ([], prop_of rrule));
+ val rlzvs = rev (Term.add_vars (prop_of rrule) []);
val vs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rlzvs, ixn)))) xs;
val rs = gen_rems (op = o pairself fst) (rlzvs, xs);
@@ -327,7 +327,7 @@
val rintrs = map (fn (intr, c) => Pattern.eta_contract
(Extraction.realizes_of thy2 vs
c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
- (rev (Term.add_vars ([], prop_of intr)) \\ params')) intr))))
+ (rev (Term.add_vars (prop_of intr) []) \\ params')) intr))))
(intrs ~~ List.concat constrss);
val rlzsets = distinct (map (fn rintr => snd (HOLogic.dest_mem
(HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs);
@@ -384,11 +384,11 @@
val (prem :: prems) = prems_of elim;
fun reorder1 (p, intr) =
Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
- (strip_all p, Term.add_vars ([], prop_of intr) \\ params');
+ (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
fun reorder2 (intr, i) =
let
val fs1 = term_vars (prop_of intr) \\ params;
- val fs2 = Term.add_vars ([], prop_of intr) \\ params'
+ val fs2 = Term.add_vars (prop_of intr) [] \\ params'
in Library.foldl (fn (t, x) => lambda (Var x) t)
(list_comb (Bound (i + length fs1), fs1), fs2)
end;
@@ -429,7 +429,7 @@
val thy5 = Extraction.add_realizers_i
(map (mk_realizer thy4 vs params')
(map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c,
- map Var (rev (Term.add_vars ([], prop_of rule)) \\ params'))))
+ map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
(List.concat (map snd rss) ~~ rintr_thms ~~ List.concat constrss))) thy4;
val elimps = List.mapPartial (fn (s, intrs) => if s mem rsets then
Option.map (rpair intrs) (find_first (fn (thm, _) =>
--- a/src/Pure/Isar/locale.ML Fri Jul 15 15:44:11 2005 +0200
+++ b/src/Pure/Isar/locale.ML Fri Jul 15 15:44:15 2005 +0200
@@ -623,7 +623,7 @@
let
val {thy, hyps, prop, maxidx, ...} = Thm.rep_thm th;
val cert = Thm.cterm_of thy;
- val (xs, Ts) = Library.split_list (Library.foldl Term.add_frees ([], prop :: hyps));
+ val (xs, Ts) = Library.split_list (fold Term.add_frees (prop :: hyps) []);
val xs' = map (rename ren) xs;
fun cert_frees names = map (cert o Free) (names ~~ Ts);
fun cert_vars names = map (cert o Var o apfst (rpair (maxidx + 1))) (names ~~ Ts);
@@ -705,7 +705,7 @@
fun frozen_tvars ctxt Ts =
let
- val tvars = rev (Library.foldl Term.add_tvarsT ([], Ts));
+ val tvars = rev (fold Term.add_tvarsT Ts []);
val tfrees = map TFree
(Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
in map (fn ((x, S), y) => (x, (S, y))) (tvars ~~ tfrees) end;
@@ -951,7 +951,7 @@
elemss;
fun inst_ax th = let
val {hyps, prop, ...} = Thm.rep_thm th;
- val ps = map (apsnd SOME) (Library.foldl Term.add_frees ([], prop :: hyps));
+ val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
val [env] = unify_parms ctxt all_params [ps];
val th' = inst_thm ctxt env th;
in th' end;
@@ -1208,7 +1208,7 @@
err "Attempt to define previously specified variable");
conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
err "Attempt to redefine variable");
- (Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths)
+ (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
end;
(* CB: for finish_elems (Int and Ext) *)
@@ -1222,7 +1222,7 @@
val spec' =
if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
else ((exts, exts'), (ints @ ts, ints' @ ts'));
- in (spec', (Library.foldl Term.add_frees (xs, ts'), env, defs)) end
+ in (spec', (fold Term.add_frees ts' xs, env, defs)) end
| eval_text ctxt (id, _) _ ((spec, binds), Defines defs) =
(spec, Library.foldl (bind_def ctxt id) (binds, map (#1 o #2) defs))
| eval_text _ _ _ (text, Notes _) = text;
@@ -1234,7 +1234,7 @@
let
fun close_frees t =
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1)
- (Term.add_frees ([], t)))
+ (Term.add_frees t []))
in Term.list_all_free (frees, t) end;
fun no_binds [] = []
@@ -1966,7 +1966,7 @@
fun sorts (a, i) = assoc (tvars, (a, i));
val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
- val vars' = Library.foldl Term.add_term_varnames (vars, vs);
+ val vars' = fold Term.add_term_varnames vs vars;
val _ = if null vars' then ()
else error ("Illegal schematic variable(s) in instantiation: " ^
commas_quote (map Syntax.string_of_vname vars'));
--- a/src/Pure/Isar/proof_context.ML Fri Jul 15 15:44:11 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Jul 15 15:44:15 2005 +0200
@@ -565,28 +565,26 @@
local
-val ins_types = foldl_aterms
- (fn (types, Free (x, T)) => Vartab.update (((x, ~1), T), types)
- | (types, Var v) => Vartab.update (v, types)
- | (types, _) => types);
+val ins_types = fold_aterms
+ (fn Free (x, T) => curry Vartab.update ((x, ~1), T)
+ | Var v => curry Vartab.update v
+ | _ => I);
-val ins_sorts = foldl_types (foldl_atyps
- (fn (sorts, TFree (x, S)) => Vartab.update (((x, ~1), S), sorts)
- | (sorts, TVar v) => Vartab.update (v, sorts)
- | (sorts, _) => sorts));
+val ins_sorts = fold_types (fold_atyps
+ (fn TFree (x, S) => curry Vartab.update ((x, ~1), S)
+ | TVar v => curry Vartab.update v
+ | _ => I));
-val ins_used = foldl_term_types (fn t => foldl_atyps
- (fn (used, TFree (x, _)) => x ins_string used
- | (used, _) => used));
+val ins_used = fold_term_types (fn t =>
+ fold_atyps (fn TFree (x, _) => insert (op =) x | _ => I));
-val ins_occs = foldl_term_types (fn t => foldl_atyps
- (fn (tab, TFree (x, _)) => Symtab.update_multi ((x, t), tab) | (tab, _) => tab));
+val ins_occs = fold_term_types (fn t =>
+ fold_atyps (fn TFree (x, _) => curry Symtab.update_multi (x, t) | _ => I));
-fun ins_skolem def_ty = foldr
- (fn ((x, x'), types) =>
- (case def_ty x' of
- SOME T => Vartab.update (((x, ~1), T), types)
- | NONE => types));
+fun ins_skolem def_ty = fold_rev (fn (x, x') =>
+ (case def_ty x' of
+ SOME T => curry Vartab.update ((x, ~1), T)
+ | NONE => I));
fun map_defaults f = map_context (fn (syntax, asms, binds, thms, cases, defs) =>
(syntax, asms, binds, thms, cases, f defs));
@@ -595,17 +593,17 @@
fun declare_term_syntax t ctxt =
ctxt
- |> map_defaults (fn (types, sorts, used, occ) => (ins_types (types, t), sorts, used, occ))
- |> map_defaults (fn (types, sorts, used, occ) => (types, ins_sorts (sorts, t), used, occ))
- |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, ins_used (used, t), occ));
+ |> map_defaults (fn (types, sorts, used, occ) => (ins_types t types, sorts, used, occ))
+ |> map_defaults (fn (types, sorts, used, occ) => (types, ins_sorts t sorts, used, occ))
+ |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, ins_used t used, occ));
fun declare_term t ctxt =
ctxt
|> declare_term_syntax t
- |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs (occ, t)))
+ |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs t occ))
|> map_defaults (fn (types, sorts, used, occ) =>
- (ins_skolem (fn x =>
- Vartab.lookup (types, (x, ~1))) types (fixes_of ctxt), sorts, used, occ));
+ (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes_of ctxt) types,
+ sorts, used, occ));
end;
@@ -676,10 +674,10 @@
(** export theorems **)
-fun get_free x (NONE, t as Free (y, _)) = if x = y then SOME t else NONE
- | get_free _ (opt, _) = opt;
+fun get_free x (t as Free (y, _)) NONE = if x = y then SOME t else NONE
+ | get_free _ _ opt = opt;
-fun find_free t x = foldl_aterms (get_free x) (NONE, t);
+fun find_free t x = fold_aterms (get_free x) t NONE;
fun export_view view is_goal inner outer =
let
@@ -1177,7 +1175,7 @@
fun fix_frees ts ctxt =
let
- val frees = Library.foldl Term.add_frees ([], ts);
+ val frees = fold Term.add_frees ts [];
fun new (x, T) = if is_fixed ctxt x then NONE else SOME ([x], SOME T);
in fix_direct false (rev (List.mapPartial new frees)) ctxt end;
--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Jul 15 15:44:11 2005 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Jul 15 15:44:15 2005 +0200
@@ -210,8 +210,7 @@
(**** eliminate definitions in proof ****)
-fun vars_of t = rev (fold_aterms
- (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
+fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
fun insert_refl defs Ts (prf1 %% prf2) =
insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
--- a/src/Pure/drule.ML Fri Jul 15 15:44:11 2005 +0200
+++ b/src/Pure/drule.ML Fri Jul 15 15:44:15 2005 +0200
@@ -958,8 +958,8 @@
(* vars in left-to-right order *)
-fun tvars_of_terms ts = rev (Library.foldl Term.add_tvars ([], ts));
-fun vars_of_terms ts = rev (Library.foldl Term.add_vars ([], ts));
+fun tvars_of_terms ts = rev (fold Term.add_tvars ts []);
+fun vars_of_terms ts = rev (fold Term.add_vars ts []);
fun tvars_of thm = tvars_of_terms [Thm.full_prop_of thm];
fun vars_of thm = vars_of_terms [Thm.full_prop_of thm];
--- a/src/Pure/meta_simplifier.ML Fri Jul 15 15:44:11 2005 +0200
+++ b/src/Pure/meta_simplifier.ML Fri Jul 15 15:44:15 2005 +0200
@@ -403,7 +403,7 @@
all its Vars? Better: a dynamic check each time a rule is applied.
*)
fun rewrite_rule_extra_vars prems elhs erhs =
- not (term_varnames erhs subset Library.foldl add_term_varnames (term_varnames elhs, prems))
+ not (term_varnames erhs subset fold add_term_varnames prems (term_varnames elhs))
orelse
not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems)));