Added term cache to function condrew in order to speed up rewriting.

--- a/src/Pure/Proof/extraction.ML	Fri Dec 10 16:55:58 2004 +0100
+++ b/src/Pure/Proof/extraction.ML	Fri Dec 10 16:57:01 2004 +0100
@@ -94,22 +94,32 @@
 
     fun rew tm =
       Pattern.rewrite_term tsig [] (condrew' :: procs) tm
-    and condrew' tm = get_first (fn (_, (prems, (tm1, tm2))) =>
+    and condrew' tm =
       let
-        fun ren t = if_none (Term.rename_abs tm1 tm t) t;
-        val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
-        val env as (Tenv, tenv) = Pattern.match tsig (inc tm1, tm);
-        val prems' = map (pairself (subst_vars env o inc o ren)) prems;
-        val env' = Envir.Envir
-          {maxidx = foldl Int.max
-            (~1, map (Int.max o pairself maxidx_of_term) prems'),
-           iTs = Vartab.make Tenv, asol = Vartab.make tenv};
-        val env'' = foldl (fn (env, p) =>
-          Pattern.unify (sign, env, [pairself rew p])) (env', prems')
-      in Some (Envir.norm_term env'' (inc (ren tm2)))
-      end handle Pattern.MATCH => None | Pattern.Unif => None)
-        (sort (Int.compare o pairself fst)
-          (Net.match_term rules (Pattern.eta_contract tm)));
+        val cache = ref ([] : (term * term) list);
+        fun lookup f x = (case assoc (!cache, x) of
+            None =>
+              let val y = f x
+              in (cache := (x, y) :: !cache; y) end
+          | Some y => y);
+      in
+        get_first (fn (_, (prems, (tm1, tm2))) =>
+        let
+          fun ren t = if_none (Term.rename_abs tm1 tm t) t;
+          val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
+          val env as (Tenv, tenv) = Pattern.match tsig (inc tm1, tm);
+          val prems' = map (pairself (subst_vars env o inc o ren)) prems;
+          val env' = Envir.Envir
+            {maxidx = foldl Int.max
+              (~1, map (Int.max o pairself maxidx_of_term) prems'),
+             iTs = Vartab.make Tenv, asol = Vartab.make tenv};
+          val env'' = foldl (fn (env, p) =>
+            Pattern.unify (sign, env, [pairself (lookup rew) p])) (env', prems')
+        in Some (Envir.norm_term env'' (inc (ren tm2)))
+        end handle Pattern.MATCH => None | Pattern.Unif => None)
+          (sort (Int.compare o pairself fst)
+            (Net.match_term rules (Pattern.eta_contract tm)))
+      end;
 
   in rew end;