src/Pure/tactic.ML
changeset 19925 3f9341831812
parent 19743 0843210d3756
child 20115 6c2ca3749a80
     1.1 --- a/src/Pure/tactic.ML	Mon Jun 19 19:56:32 2006 +0200
     1.2 +++ b/src/Pure/tactic.ML	Mon Jun 19 20:21:30 2006 +0200
     1.3 @@ -133,12 +133,16 @@
     1.4  
     1.5  (*Makes a rule by applying a tactic to an existing rule*)
     1.6  fun rule_by_tactic tac rl =
     1.7 -  let val (st, thaw) = freeze_thaw_robust (zero_var_indexes rl)
     1.8 -  in case Seq.pull (tac st)  of
     1.9 -        NONE        => raise THM("rule_by_tactic", 0, [rl])
    1.10 -      | SOME(st',_) => Thm.varifyT (thaw 0 st')
    1.11 +  let
    1.12 +    val ctxt = Variable.thm_context rl;
    1.13 +    val ([st], ctxt') = Variable.import true [rl] ctxt;
    1.14 +  in
    1.15 +    (case Seq.pull (tac st) of
    1.16 +      NONE => raise THM ("rule_by_tactic", 0, [rl])
    1.17 +    | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st'))
    1.18    end;
    1.19  
    1.20 +
    1.21  (*** Basic tactics ***)
    1.22  
    1.23  (*** The following fail if the goal number is out of range: