# HG changeset patch
# User wenzelm
# Date 1254432425 -7200
# Node ID c8f5a7c8353fb4dbf6002cbfc557f5bb09fb80df
# Parent  98702c579ad0f62b7349a840c0e0043facc78b38
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;

diff -r 98702c579ad0 -r c8f5a7c8353f src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Thu Oct 01 22:40:29 2009 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Thu Oct 01 23:27:05 2009 +0200
@@ -538,7 +538,7 @@
    val nnf_norm_conv' = 
      nnf_conv then_conv 
      literals_conv [@{term "op &"}, @{term "op |"}] [] 
-     (More_Conv.cache_conv 
+     (Conv.cache_conv 
        (first_conv [real_lt_conv, real_le_conv, 
                     real_eq_conv, real_not_lt_conv, 
                     real_not_le_conv, real_not_eq_conv, all_conv]))
diff -r 98702c579ad0 -r c8f5a7c8353f src/Pure/conv.ML
--- a/src/Pure/conv.ML	Thu Oct 01 22:40:29 2009 +0200
+++ b/src/Pure/conv.ML	Thu Oct 01 23:27:05 2009 +0200
@@ -1,5 +1,6 @@
 (*  Title:      Pure/conv.ML
-    Author:     Amine Chaieb and Makarius
+    Author:     Amine Chaieb, TU Muenchen
+    Author:     Makarius
 
 Conversions: primitive equality reasoning.
 *)
@@ -22,6 +23,7 @@
   val every_conv: conv list -> conv
   val try_conv: conv -> conv
   val repeat_conv: conv -> conv
+  val cache_conv: conv -> conv
   val abs_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
   val combination_conv: conv -> conv -> conv
   val comb_conv: conv -> conv
@@ -44,7 +46,7 @@
 structure Conv: CONV =
 struct
 
-(* conversionals *)
+(* basic conversionals *)
 
 fun no_conv _ = raise CTERM ("no conversion", []);
 val all_conv = Thm.reflexive;
@@ -72,6 +74,8 @@
 fun try_conv cv = cv else_conv all_conv;
 fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
 
+fun cache_conv (cv: conv) = Thm.cterm_cache cv;
+
 
 
 (** Pure conversions **)
@@ -177,5 +181,5 @@
 
 end;
 
-structure BasicConv: BASIC_CONV = Conv;
-open BasicConv;
+structure Basic_Conv: BASIC_CONV = Conv;
+open Basic_Conv;
diff -r 98702c579ad0 -r c8f5a7c8353f src/Tools/more_conv.ML
--- a/src/Tools/more_conv.ML	Thu Oct 01 22:40:29 2009 +0200
+++ b/src/Tools/more_conv.ML	Thu Oct 01 23:27:05 2009 +0200
@@ -1,5 +1,5 @@
-(* Title:  Tools/more_conv.ML
-   Author: Sascha Boehme
+(*  Title:       Tools/more_conv.ML
+    Author:      Sascha Boehme, TU Muenchen
 
 Further conversions and conversionals.
 *)
@@ -14,16 +14,11 @@
   val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
 
   val binder_conv: (Proof.context -> conv) -> Proof.context -> conv
-
-  val cache_conv: conv -> conv
 end
 
-
-
 structure More_Conv : MORE_CONV =
 struct
 
-
 fun rewrs_conv eqs = Conv.first_conv (map Conv.rewr_conv eqs)
 
 
@@ -45,19 +40,4 @@
 fun binder_conv cv ctxt =
   Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt)
 
-
-fun cache_conv conv =
-  let
-    val cache = Synchronized.var "cache_conv" Termtab.empty
-    fun lookup t =
-      Synchronized.change_result cache (fn tab => (Termtab.lookup tab t, tab))
-    val keep = Synchronized.change cache o Termtab.insert Thm.eq_thm
-    fun keep_result t thm = (keep (t, thm); thm)
-
-    fun cconv ct =
-      (case lookup (Thm.term_of ct) of
-        SOME thm => thm
-      | NONE => keep_result (Thm.term_of ct) (conv ct))
-  in cconv end
-
 end