# HG changeset patch
# User haftmann
# Date 1282554588 -7200
# Node ID e8236c4aff1679875f2876782bed0180a5c3269f
# Parent  8494cb38cbf7c3b22dfc15a870536918039c7879
tap_thy conversional

diff -r 8494cb38cbf7 -r e8236c4aff16 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Mon Aug 23 11:09:48 2010 +0200
+++ b/src/Pure/conv.ML	Mon Aug 23 11:09:48 2010 +0200
@@ -48,6 +48,7 @@
   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 =
@@ -211,6 +212,9 @@
       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;