src/Pure/conv.ML

   val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
   val prems_conv: int -> conv -> conv
   val concl_conv: int -> conv -> conv
   val fconv_rule: conv -> thm -> thm
   val gconv_rule: conv -> int -> thm -> thm
+  val tap_thy: (theory -> conv) -> conv
 end;
 
 structure Conv: CONV =
 struct
 

         if Thm.is_reflexive eq then th
         else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th
       end
   | NONE => raise THM ("gconv_rule", i, [th]));
 
+
+fun tap_thy conv ct = conv (Thm.theory_of_cterm ct) ct;
+
 end;
 
 structure Basic_Conv: BASIC_CONV = Conv;
 open Basic_Conv;