--- 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]))
--- 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;
--- 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