src/Pure/tactic.ML
changeset 22568 ed7aa5a350ef
parent 22560 f19ddf96c323
child 22583 4b1ecb19b411
     1.1 --- a/src/Pure/tactic.ML	Tue Apr 03 19:24:11 2007 +0200
     1.2 +++ b/src/Pure/tactic.ML	Tue Apr 03 19:24:13 2007 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  fun rule_by_tactic tac rl =
     1.5    let
     1.6      val ctxt = Variable.thm_context rl;
     1.7 -    val ((_, [st]), ctxt') = Variable.import true [rl] ctxt;
     1.8 +    val ((_, [st]), ctxt') = Variable.import_thms true [rl] ctxt;
     1.9    in
    1.10      (case Seq.pull (tac st) of
    1.11        NONE => raise THM ("rule_by_tactic", 0, [rl])