# HG changeset patch
# User wenzelm
# Date 1121435055 -7200
# Node ID 7446b4be013b23bcf253c8e9bc60109d0217737d
# Parent  43abdba4da5cd642df6d55eb7507087850ea9fc6
tuned fold on terms;

diff -r 43abdba4da5c -r 7446b4be013b src/HOL/Library/EfficientNat.thy
--- 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' []
diff -r 43abdba4da5c -r 7446b4be013b src/HOL/Orderings.thy
--- 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] =
diff -r 43abdba4da5c -r 7446b4be013b src/HOL/Tools/inductive_codegen.ML
--- 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)
diff -r 43abdba4da5c -r 7446b4be013b src/HOL/Tools/inductive_package.ML
--- 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))
diff -r 43abdba4da5c -r 7446b4be013b src/HOL/Tools/inductive_realizer.ML
--- 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, _) =>
diff -r 43abdba4da5c -r 7446b4be013b src/Pure/Isar/locale.ML
--- 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'));
diff -r 43abdba4da5c -r 7446b4be013b src/Pure/Isar/proof_context.ML
--- 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;
 
diff -r 43abdba4da5c -r 7446b4be013b src/Pure/Proof/proof_rewrite_rules.ML
--- 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
diff -r 43abdba4da5c -r 7446b4be013b src/Pure/drule.ML
--- 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];
diff -r 43abdba4da5c -r 7446b4be013b src/Pure/meta_simplifier.ML
--- 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)));