src/Pure/conv.ML
changeset 38668 e8236c4aff16
parent 36936 c52d1c130898
child 41248 bb28bf635202
     1.1 --- a/src/Pure/conv.ML	Mon Aug 23 11:09:48 2010 +0200
     1.2 +++ b/src/Pure/conv.ML	Mon Aug 23 11:09:48 2010 +0200
     1.3 @@ -48,6 +48,7 @@
     1.4    val concl_conv: int -> conv -> conv
     1.5    val fconv_rule: conv -> thm -> thm
     1.6    val gconv_rule: conv -> int -> thm -> thm
     1.7 +  val tap_thy: (theory -> conv) -> conv
     1.8  end;
     1.9  
    1.10  structure Conv: CONV =
    1.11 @@ -211,6 +212,9 @@
    1.12        end
    1.13    | NONE => raise THM ("gconv_rule", i, [th]));
    1.14  
    1.15 +
    1.16 +fun tap_thy conv ct = conv (Thm.theory_of_cterm ct) ct;
    1.17 +
    1.18  end;
    1.19  
    1.20  structure Basic_Conv: BASIC_CONV = Conv;