1.1 --- a/src/Pure/conv.ML	Fri Dec 17 18:24:44 2010 +0100
     1.2 +++ b/src/Pure/conv.ML	Fri Dec 17 18:32:40 2010 +0100
     1.3 @@ -48,7 +48,6 @@
     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 @@ -212,9 +211,6 @@
    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;