# HG changeset patch
# User haftmann
# Date 1121247037 -7200
# Node ID be2780f435e1c51be5c89c2524320722ca02e078
# Parent  e8f7a6ec92e5dc6772e98014c8ee66744a3145dc
(fix for an accidental commit)

diff -r e8f7a6ec92e5 -r be2780f435e1 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Jul 13 11:29:08 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Jul 13 11:30:37 2005 +0200
@@ -705,7 +705,7 @@
 
 fun frozen_tvars ctxt Ts =
   let
-    val tvars = rev (fold Term.add_tvarsT Ts []);
+    val tvars = rev (Library.foldl 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;
diff -r e8f7a6ec92e5 -r be2780f435e1 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jul 13 11:29:08 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jul 13 11:30:37 2005 +0200
@@ -565,25 +565,22 @@
 
 local
 
-val ins_types = 
-  let fun ins_types' (Free (x, T)) types = Vartab.update (((x, ~1), T), types)
-         | ins_types' (Var v) types = Vartab.update (v, types)
-         | ins_types' _ types = types
-  in fold_aterms ins_types' end;
+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_sorts =
-  let fun ins_sorts' (TFree (x, S)) sorts = Vartab.update (((x, ~1), S), sorts)
-         | ins_sorts' (TVar v) sorts = Vartab.update (v, sorts)
-         | ins_sorts' _ sorts = sorts
-  in fold_types ins_sorts' end;
+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_used = fold_term_types (fn t => fold_atyps
-  (fn TFree (x, _) => curry (op ins_string) x
-    | _ => I));
+val ins_used = foldl_term_types (fn t => foldl_atyps
+  (fn (used, TFree (x, _)) => x ins_string used
+    | (used, _) => used));
 
-val ins_occs = fold_term_types (fn t => fold_atyps
-  (fn TFree (x, _) => curry Symtab.update_multi (x, t)
-    | _ => I));
+val ins_occs = foldl_term_types (fn t => foldl_atyps
+  (fn (tab, TFree (x, _)) => Symtab.update_multi ((x, t), tab) | (tab, _) => tab));
 
 fun ins_skolem def_ty = foldr
   (fn ((x, x'), types) =>
@@ -598,14 +595,14 @@
 
 fun declare_term_syntax t ctxt =
   ctxt
-  |> 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));
+  |> 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));
 
 fun declare_term t ctxt =
   ctxt
   |> declare_term_syntax t
-  |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs t occ))
+  |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs (occ, t)))
   |> map_defaults (fn (types, sorts, used, occ) =>
       (ins_skolem (fn x =>
         Vartab.lookup (types, (x, ~1))) types (fixes_of ctxt), sorts, used, occ));
@@ -679,10 +676,10 @@
 
 (** export theorems **)
 
-fun find_free t x =
-  let fun get_free (t as Free (y, _)) NONE = if x = y then SOME t else NONE
-         | get_free _ opt = opt
-  in fold_aterms get_free t NONE end;
+fun get_free x (NONE, t as Free (y, _)) = 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 export_view view is_goal inner outer =
   let
diff -r e8f7a6ec92e5 -r be2780f435e1 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Wed Jul 13 11:29:08 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Wed Jul 13 11:30:37 2005 +0200
@@ -128,8 +128,8 @@
 
 fun msg d s = priority (Symbol.spaces d ^ s);
 
-fun vars_of t = rev (fold_aterms
-  (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
+fun vars_of t = rev (foldl_aterms
+  (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
 
 fun vfs_of t = vars_of t @ sort (make_ord atless) (term_frees t);
 
diff -r e8f7a6ec92e5 -r be2780f435e1 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Jul 13 11:29:08 2005 +0200
+++ b/src/Pure/drule.ML	Wed Jul 13 11:30:37 2005 +0200
@@ -958,7 +958,7 @@
 
 (* vars in left-to-right order *)
 
-fun tvars_of_terms ts = rev (fold Term.add_tvars ts []);
+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 thm = tvars_of_terms [Thm.full_prop_of thm];
diff -r e8f7a6ec92e5 -r be2780f435e1 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Jul 13 11:29:08 2005 +0200
+++ b/src/Pure/term.ML	Wed Jul 13 11:30:37 2005 +0200
@@ -161,6 +161,10 @@
   val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
   val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
   val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
+  val foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a
+  val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
+  val foldl_term_types: (term -> 'a * typ -> 'a) -> 'a * term -> 'a
+  val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
   val add_term_names: term * string list -> string list
   val add_term_varnames: indexname list * term -> indexname list
   val term_varnames: term -> indexname list
@@ -191,9 +195,13 @@
   val map_typ: (string -> string) -> (string -> string) -> typ -> typ
   val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
   val dest_abs: string * typ * term -> string * term
-  val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
+  (*val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
   val add_vars: (indexname * typ) list * term -> (indexname * typ) list
+  val add_frees: (string * typ) list * term -> (string * typ) list*)
+  val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
+  val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
+  val add_vars: (indexname * typ) list * term -> (indexname * typ) list
   val add_frees: (string * typ) list * term -> (string * typ) list
   val dummy_patternN: string
   val no_dummy_patterns: term -> term
@@ -1187,16 +1195,16 @@
 
 (* left-ro-right traversal *)
 
-(*foldl atoms of type*)
+(*fold atoms of type*)
 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   | fold_atyps f T = f T
 
-(*foldl atoms of term*)
+(*fold atoms of term*)
 fun fold_aterms f (t $ u) = (fold_aterms f u) o (fold_aterms f t)
   | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   | fold_aterms f t = f t;
 
-(*foldl types of term*)
+(*fold types of term*)
 fun fold_term_types f (t as Const (_, T)) = f t T
   | fold_term_types f (t as Free (_, T)) = f t T
   | fold_term_types f (t as Var (_, T)) = f t T
@@ -1206,7 +1214,26 @@
 
 fun fold_types f = fold_term_types (fn _ => f);
 
-(*collect variables*)
+(*foldl atoms of type*)
+fun foldl_atyps f (x, Type (_, Ts)) = Library.foldl (foldl_atyps f) (x, Ts)
+  | foldl_atyps f x_atom = f x_atom;
+
+(*foldl atoms of term*)
+fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u)
+  | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t)
+  | foldl_aterms f x_atom = f x_atom;
+
+(*foldl types of term*)
+fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T)
+  | foldl_term_types f (x, t as Free (_, T)) = f t (x, T)
+  | foldl_term_types f (x, t as Var (_, T)) = f t (x, T)
+  | foldl_term_types f (x, Bound _) = x
+  | foldl_term_types f (x, t as Abs (_, T, b)) = foldl_term_types f (f t (x, T), b)
+  | foldl_term_types f (x, t $ u) = foldl_term_types f (foldl_term_types f (x, t), u);
+
+fun foldl_types f = foldl_term_types (fn _ => f);
+
+(*(*collect variables*)
 val add_tvarsT =
   let fun add_tvarsT' (TVar v) = insert (op =) v
          | add_tvarsT' _ = I
@@ -1219,7 +1246,7 @@
 val add_frees =
   let fun add_frees' (Free v) = insert (op =) v
          | add_frees' _ = I
-  in uncurry (fold_aterms add_frees') o swap end;
+  in uncurry (fold_aterms add_frees') o swap end;*)
 
 (*collect variable names*)
 val add_term_varnames =
@@ -1227,6 +1254,16 @@
          | add_term_varnames' _ xs = xs
   in uncurry (fold_aterms add_term_varnames') o swap end;
   
+fun term_varnames t = add_term_varnames ([], t);*)
+
+(*collect variables*)
+val add_tvarsT = foldl_atyps (fn (vs, TVar v) => insert (op =) v vs | (vs, _) => vs);
+val add_tvars = foldl_types add_tvarsT;
+val add_vars = foldl_aterms (fn (vs, Var v) => insert (op =) v vs | (vs, _) => vs);
+val add_frees = foldl_aterms (fn (vs, Free v) => insert (op =) v vs | (vs, _) => vs);
+
+(*collect variable names*)
+val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
 fun term_varnames t = add_term_varnames ([], t);