1.1 --- a/src/Pure/conv.ML	Thu Oct 04 16:59:29 2007 +0200
     1.2 +++ b/src/Pure/conv.ML	Thu Oct 04 16:59:30 2007 +0200
     1.3 @@ -18,8 +18,7 @@
     1.4    val every_conv: conv list -> conv
     1.5    val try_conv: conv -> conv
     1.6    val repeat_conv: conv -> conv
     1.7 -  val cache_conv: conv -> conv
     1.8 -  val abs_conv: conv -> conv
     1.9 +  val abs_conv: (Proof.context -> conv) -> Proof.context -> conv
    1.10    val combination_conv: conv -> conv -> conv
    1.11    val comb_conv: conv -> conv
    1.12    val arg_conv: conv -> conv
    1.13 @@ -27,7 +26,7 @@
    1.14    val arg1_conv: conv -> conv
    1.15    val fun2_conv: conv -> conv
    1.16    val binop_conv: conv -> conv
    1.17 -  val forall_conv: int -> conv -> conv
    1.18 +  val forall_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
    1.19    val concl_conv: int -> conv -> conv
    1.20    val prems_conv: int -> conv -> conv
    1.21    val fconv_rule: conv -> thm -> thm
    1.22 @@ -65,29 +64,19 @@
    1.23  fun try_conv cv = cv else_conv all_conv;
    1.24  fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
    1.25  
    1.26 -fun cache_conv cv =
    1.27 -  let
    1.28 -    val cache = ref Termtab.empty;
    1.29 -    fun conv ct =
    1.30 -      (case Termtab.lookup (! cache) (Thm.term_of ct) of
    1.31 -        SOME th => th
    1.32 -      | NONE =>
    1.33 -          let val th = cv ct
    1.34 -          in change cache (Termtab.update (Thm.term_of ct, th)); th end);
    1.35 - in conv end;
    1.36 -
    1.37  
    1.38  
    1.39  (** Pure conversions **)
    1.40  
    1.41  (* lambda terms *)
    1.42  
    1.43 -fun abs_conv cv ct =
    1.44 +fun abs_conv cv ctxt ct =
    1.45    (case Thm.term_of ct of
    1.46      Abs (x, _, _) =>
    1.47        let
    1.48 -        val (v, ct') = Thm.dest_abs (SOME (gensym "gensym_abs_")) ct;
    1.49 -        val eq = cv ct';
    1.50 +        val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
    1.51 +        val (v, ct') = Thm.dest_abs (SOME u) ct;
    1.52 +        val eq = (cv ctxt') ct';
    1.53        in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
    1.54    | _ => raise CTERM ("abs_conv", [ct]));
    1.55  
    1.56 @@ -108,10 +97,10 @@
    1.57  (* logic *)
    1.58  
    1.59  (*rewrite B in !!x1 ... xn. B*)
    1.60 -fun forall_conv n cv ct =
    1.61 +fun forall_conv n cv ctxt ct =
    1.62    if n <> 0 andalso can Logic.dest_all (Thm.term_of ct)
    1.63 -  then arg_conv (abs_conv (forall_conv (n - 1) cv)) ct
    1.64 -  else cv ct;
    1.65 +  then arg_conv (abs_conv (forall_conv (n - 1) cv) ctxt) ct
    1.66 +  else cv ctxt ct;
    1.67  
    1.68  (*rewrite B in A1 ==> ... ==> An ==> B*)
    1.69  fun concl_conv 0 cv ct = cv ct