# HG changeset patch
# User wenzelm
# Date 1292607513 -3600
# Node ID 4ae674714876fe682b3e7bae3ccf12c2e609fd78
# Parent  bb28bf63520262edda9f84dde7ec4acf248aaedf# Parent  1e6d86821718b13597693ae1f8ab13d4c3828c61
merged

diff -r 1e6d86821718 -r 4ae674714876 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Fri Dec 17 18:33:35 2010 +0100
+++ b/src/Pure/conv.ML	Fri Dec 17 18:38:33 2010 +0100
@@ -48,7 +48,6 @@
   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 =
@@ -212,9 +211,6 @@
       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;