# HG changeset patch
# User wenzelm
# Date 1121435060 -7200
# Node ID fb39dcfc1c24ddb1b36fbcf419ed019461ddb53d
# Parent  0f536ece46e352b953101488ebc8dbc4cf514e58
tuned fold on terms;
tuned assoc;

diff -r 0f536ece46e3 -r fb39dcfc1c24 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Jul 15 15:44:19 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Jul 15 15:44:20 2005 +0200
@@ -95,7 +95,7 @@
     and condrew' tm =
       let
         val cache = ref ([] : (term * term) list);
-        fun lookup f x = (case assoc (!cache, x) of
+        fun lookup f x = (case gen_assoc (op =) (!cache, x) of
             NONE =>
               let val y = f x
               in (cache := (x, y) :: !cache; y) end
@@ -128,9 +128,7 @@
 
 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 _ => insert (op =) v | _ => I) t []);
 fun vfs_of t = vars_of t @ sort (make_ord atless) (term_frees t);
 
 fun forall_intr (t, prop) =
@@ -161,13 +159,13 @@
 
 fun get_var_type t =
   let
-    val vs = Term.add_vars ([], t);
-    val fs = Term.add_frees ([], t)
+    val vs = Term.add_vars t [];
+    val fs = Term.add_frees t [];
   in fn 
-      Var (ixn, _) => (case assoc (Term.add_vars ([], t), ixn) of
+      Var (ixn, _) => (case assoc_string_int (vs, ixn) of
           NONE => error "get_var_type: no such variable in term"
         | SOME T => Var (ixn, T))
-    | Free (s, _) => (case assoc (Term.add_frees ([], t), s) of
+    | Free (s, _) => (case assoc_string (fs, s) of
           NONE => error "get_var_type: no such variable in term"
         | SOME T => Free (s, T))
     | _ => error "get_var_type: not a variable"
@@ -537,7 +535,7 @@
                   (Bound (length Us), eT :: Us);
                 val u = list_comb (incr_boundvars (length Us') t,
                   map Bound (length Us - 1 downto 0));
-                val u' = (case assoc (types, tname_of T) of
+                val u' = (case assoc_string (types, tname_of T) of
                     SOME ((_, SOME f)) => f r eT u T
                   | _ => Const ("realizes", eT --> T --> T) $ r $ u)
               in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end