src/Pure/tactic.ML

--- a/src/Pure/tactic.ML	Mon Jun 19 19:56:32 2006 +0200
+++ b/src/Pure/tactic.ML	Mon Jun 19 20:21:30 2006 +0200
@@ -133,12 +133,16 @@
 
 (*Makes a rule by applying a tactic to an existing rule*)
 fun rule_by_tactic tac rl =
-  let val (st, thaw) = freeze_thaw_robust (zero_var_indexes rl)
-  in case Seq.pull (tac st)  of
-        NONE        => raise THM("rule_by_tactic", 0, [rl])
-      | SOME(st',_) => Thm.varifyT (thaw 0 st')
+  let
+    val ctxt = Variable.thm_context rl;
+    val ([st], ctxt') = Variable.import true [rl] ctxt;
+  in
+    (case Seq.pull (tac st) of
+      NONE => raise THM ("rule_by_tactic", 0, [rl])
+    | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st'))
   end;
 
+
 (*** Basic tactics ***)
 
 (*** The following fail if the goal number is out of range: