src/Pure/tactic.ML

--- a/src/Pure/tactic.ML	Tue Apr 03 19:24:11 2007 +0200
+++ b/src/Pure/tactic.ML	Tue Apr 03 19:24:13 2007 +0200
@@ -118,7 +118,7 @@
 fun rule_by_tactic tac rl =
   let
     val ctxt = Variable.thm_context rl;
-    val ((_, [st]), ctxt') = Variable.import true [rl] ctxt;
+    val ((_, [st]), ctxt') = Variable.import_thms true [rl] ctxt;
   in
     (case Seq.pull (tac st) of
       NONE => raise THM ("rule_by_tactic", 0, [rl])