# HG changeset patch
# User haftmann
# Date 1125669287 -7200
# Node ID 148c241d2492991637c0016db54273efe95796d7
# Parent  f42bc4f7afdfe4b43dcf603a21b818d05dea9cd1
some 'assoc' etc. refactoring

diff -r f42bc4f7afdf -r 148c241d2492 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Sep 02 15:25:44 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Sep 02 15:54:47 2005 +0200
@@ -93,7 +93,7 @@
     and condrew' tm =
       let
         val cache = ref ([] : (term * term) list);
-        fun lookup f x = (case gen_assoc (op =) (!cache, x) of
+        fun lookup f x = (case AList.lookup (op =) (!cache) x of
             NONE =>
               let val y = f x
               in (cache := (x, y) :: !cache; y) end
@@ -160,10 +160,10 @@
     val vs = Term.add_vars t [];
     val fs = Term.add_frees t [];
   in fn 
-      Var (ixn, _) => (case assoc_string_int (vs, ixn) of
+      Var (ixn, _) => (case AList.lookup (op =) vs ixn of
           NONE => error "get_var_type: no such variable in term"
         | SOME T => Var (ixn, T))
-    | Free (s, _) => (case assoc_string (fs, s) of
+    | Free (s, _) => (case AList.lookup (op =) 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"
diff -r f42bc4f7afdf -r 148c241d2492 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Fri Sep 02 15:25:44 2005 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Fri Sep 02 15:54:47 2005 +0200
@@ -357,7 +357,7 @@
             fun inc i =
               map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i);
             val (maxidx', prf, prfs') =
-              (case gen_assoc (op =) (prfs, (a, prop)) of
+              (case AList.lookup (op =) prfs (a, prop) of
                 NONE =>
                   let
                     val _ = message ("Reconstructing proof of " ^ a);
diff -r f42bc4f7afdf -r 148c241d2492 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Fri Sep 02 15:25:44 2005 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri Sep 02 15:54:47 2005 +0200
@@ -970,7 +970,7 @@
                    val (h, ts) = strip_comb t
                in case cong_name h of
                     SOME a =>
-                      (case assoc_string (fst congs, a) of
+                      (case AList.lookup (op =) (fst congs) a of
                          NONE => appc ()
                        | SOME cong =>
   (*post processing: some partial applications h t1 ... tj, j <= length ts,