# HG changeset patch
# User wenzelm
# Date 1191509970 -7200
# Node ID 5684cbf8c89569231ba3568ff7b9ec80cf507462
# Parent  9131433b19bb0d732c15208a073ef9f837410992
abs_conv/forall_conv: proper context (avoid gensym);
removed unused cache_conv;

diff -r 9131433b19bb -r 5684cbf8c895 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Thu Oct 04 16:59:29 2007 +0200
+++ b/src/Pure/conv.ML	Thu Oct 04 16:59:30 2007 +0200
@@ -18,8 +18,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: conv -> conv
+  val abs_conv: (Proof.context -> conv) -> Proof.context -> conv
   val combination_conv: conv -> conv -> conv
   val comb_conv: conv -> conv
   val arg_conv: conv -> conv
@@ -27,7 +26,7 @@
   val arg1_conv: conv -> conv
   val fun2_conv: conv -> conv
   val binop_conv: conv -> conv
-  val forall_conv: int -> conv -> conv
+  val forall_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
   val concl_conv: int -> conv -> conv
   val prems_conv: int -> conv -> conv
   val fconv_rule: conv -> thm -> thm
@@ -65,29 +64,19 @@
 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 =
-  let
-    val cache = ref Termtab.empty;
-    fun conv ct =
-      (case Termtab.lookup (! cache) (Thm.term_of ct) of
-        SOME th => th
-      | NONE =>
-          let val th = cv ct
-          in change cache (Termtab.update (Thm.term_of ct, th)); th end);
- in conv end;
-
 
 
 (** Pure conversions **)
 
 (* lambda terms *)
 
-fun abs_conv cv ct =
+fun abs_conv cv ctxt ct =
   (case Thm.term_of ct of
     Abs (x, _, _) =>
       let
-        val (v, ct') = Thm.dest_abs (SOME (gensym "gensym_abs_")) ct;
-        val eq = cv ct';
+        val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
+        val (v, ct') = Thm.dest_abs (SOME u) ct;
+        val eq = (cv ctxt') ct';
       in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
   | _ => raise CTERM ("abs_conv", [ct]));
 
@@ -108,10 +97,10 @@
 (* logic *)
 
 (*rewrite B in !!x1 ... xn. B*)
-fun forall_conv n cv ct =
+fun forall_conv n cv ctxt ct =
   if n <> 0 andalso can Logic.dest_all (Thm.term_of ct)
-  then arg_conv (abs_conv (forall_conv (n - 1) cv)) ct
-  else cv ct;
+  then arg_conv (abs_conv (forall_conv (n - 1) cv) ctxt) ct
+  else cv ctxt ct;
 
 (*rewrite B in A1 ==> ... ==> An ==> B*)
 fun concl_conv 0 cv ct = cv ct