(intermediate commit)

--- a/src/Pure/Isar/induct_attrib.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/Isar/induct_attrib.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -56,7 +56,7 @@
 local
 
 fun rev_vars_of tm =
-  Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm)
+  Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []
   |> Library.distinct;
 
 val mk_var = encode_type o #2 o Term.dest_Var;

--- a/src/Pure/Isar/locale.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -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;

--- a/src/Pure/Isar/obtain.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -89,8 +89,8 @@
     val bound_thesis_raw as (bound_thesis_name, _) =
       Term.dest_Free (bind_thesis (Free (thesisN, propT)));
     val bound_thesis_var =
-      foldl_aterms (fn (v, Free (x, T)) => if x = bound_thesis_name then (x, T) else v
-        | (v, t) => v) (bound_thesis_raw, bound_thesis);
+      fold_aterms (fn Free (x, T) => (fn v => if x = bound_thesis_name then (x, T) else v)
+        | _ => I) bound_thesis bound_thesis_raw;
 
     fun occs_var x = Library.get_first (fn t =>
       ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;

--- a/src/Pure/Isar/proof_context.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -565,22 +565,25 @@
 
 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 = 
+  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_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 =
+  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_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, _) => curry (op ins_string) 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) =>
@@ -595,14 +598,14 @@
 
 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));
@@ -676,10 +679,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 find_free t x = foldl_aterms (get_free x) (NONE, t);
+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 export_view view is_goal inner outer =
   let

--- a/src/Pure/Proof/extraction.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -128,8 +128,8 @@
 
 fun msg d s = priority (Symbol.spaces d ^ s);
 
-fun vars_of t = rev (foldl_aterms
-  (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
+fun vars_of t = rev (fold_aterms
+  (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
 
 fun vfs_of t = vars_of t @ sort (make_ord atless) (term_frees t);
 

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -210,8 +210,8 @@
 
 (**** eliminate definitions in proof ****)
 
-fun vars_of t = rev (foldl_aterms
-  (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
+fun vars_of t = rev (fold_aterms
+  (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
 
 fun insert_refl defs Ts (prf1 %% prf2) =
       insert_refl defs Ts prf1 %% insert_refl defs Ts prf2

--- a/src/Pure/Proof/reconstruct.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -23,8 +23,8 @@
 val quiet_mode = ref true;
 fun message s = if !quiet_mode then () else writeln s;
 
-fun vars_of t = rev (foldl_aterms
-  (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
+fun vars_of t = rev (fold_aterms
+  (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
 
 fun forall_intr (t, prop) =
   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)

--- a/src/Pure/drule.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/drule.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -958,7 +958,7 @@
 
 (* vars in left-to-right order *)
 
-fun tvars_of_terms ts = rev (Library.foldl Term.add_tvars ([], ts));
+fun tvars_of_terms ts = rev (fold 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];

--- a/src/Pure/goals.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/goals.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -350,10 +350,10 @@
 
 (* prepare props *)
 
-val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
+val add_frees = fold_aterms (fn Free v => (fn vs => v ins vs) | _ => I);
 
 fun enter_term t (envS, envT, used) =
-  (Term.add_term_tfrees (t, envS), add_frees (envT, t), Term.add_term_tfree_names (t, used));
+  (Term.add_term_tfrees (t, envS), add_frees t envT, Term.add_term_tfree_names (t, used));
 
 fun read_axm thy ((envS, envT, used), (name, s)) =
   let

--- a/src/Pure/proofterm.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/proofterm.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -766,8 +766,8 @@
 
 (***** axioms and theorems *****)
 
-fun vars_of t = rev (foldl_aterms
-  (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
+fun vars_of t = rev (fold_aterms
+  (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
 
 fun test_args _ [] = true
   | test_args is (Bound i :: ts) =

--- a/src/Pure/pure_thy.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/pure_thy.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -394,8 +394,8 @@
 fun forall_elim_vars_aux strip_vars i th =
   let
     val {thy, tpairs, prop, ...} = Thm.rep_thm th;
-    fun add_used t used = (used, t) |> Term.foldl_aterms
-      (fn (xs, Var ((x, j), _)) => if i = j then x ins_string xs else xs | (xs, _) => xs);
+    val add_used = Term.fold_aterms
+      (fn Var ((x, j), _) => if i = j then curry (op ins_string) x else I | _ => I);
     val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []);
     val vars = strip_vars prop;
     val cvars = (Term.variantlist (map #1 vars, used), vars)

--- a/src/Pure/term.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/term.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -157,10 +157,10 @@
   val term_frees: term -> term list
   val variant_abs: string * typ * term -> string * term
   val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
-  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 fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
+  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 add_term_names: term * string list -> string list
   val add_term_varnames: indexname list * term -> indexname list
   val term_varnames: term -> indexname list
@@ -191,8 +191,8 @@
   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: (indexname * sort) list * typ -> (indexname * sort) list
-  val add_tvars: (indexname * sort) list * term -> (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 dummy_patternN: string
@@ -1188,32 +1188,45 @@
 (* left-ro-right traversal *)
 
 (*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;
+fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
+  | fold_atyps f T = f T
 
 (*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;
+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*)
-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 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
+  | fold_term_types f (Bound _) = I
+  | fold_term_types f (t as Abs (_, T, b)) = (fold_term_types f b) o (f t T)
+  | fold_term_types f (t $ u) = (fold_term_types f u) o (fold_term_types f t);
 
-fun foldl_types f = foldl_term_types (fn _ => f);
+fun fold_types f = fold_term_types (fn _ => f);
 
 (*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);
+val add_tvarsT =
+  let fun add_tvarsT' (TVar v) = insert (op =) v
+         | add_tvarsT' _ = I
+  in fold_atyps add_tvarsT' end;
+val add_tvars = fold_types add_tvarsT;
+val add_vars =
+  let fun add_vars' (Var v) = insert (op =) v
+         | add_vars' _ = I
+  in uncurry (fold_aterms add_vars') o swap end;
+val add_frees =
+  let fun add_frees' (Free v) = insert (op =) v
+         | add_frees' _ = I
+  in uncurry (fold_aterms add_frees') o swap end;
 
 (*collect variable names*)
-val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
+val add_term_varnames =
+  let fun add_term_varnames' (Var (x, _)) xs = ins_ix (x, xs)
+         | add_term_varnames' _ xs = xs
+  in uncurry (fold_aterms add_term_varnames') o swap end;
+  
 fun term_varnames t = add_term_varnames ([], t);
 
 
@@ -1258,7 +1271,7 @@
   | is_dummy_pattern _ = false;
 
 fun no_dummy_patterns tm =
-  if not (foldl_aterms (fn (b, t) => b orelse is_dummy_pattern t) (false, tm)) then tm
+  if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
 
 fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =