changeset 31794 | 71af1fd6a5e4 |
parent 31251 | 6ff48aa6142c |
child 31945 | d5f186aa0bed |
--- a/src/Pure/tactic.ML Wed Jun 24 20:52:49 2009 +0200 +++ b/src/Pure/tactic.ML Wed Jun 24 21:28:02 2009 +0200 @@ -91,7 +91,7 @@ fun rule_by_tactic tac rl = let val ctxt = Variable.thm_context rl; - val ((_, [st]), ctxt') = Variable.import_thms true [rl] ctxt; + val ((_, [st]), ctxt') = Variable.import true [rl] ctxt; in (case Seq.pull (tac st) of NONE => raise THM ("rule_by_tactic", 0, [rl])