src/Pure/tactic.ML
changeset 19743 0843210d3756
parent 19532 dae447f2b0b4
child 19925 3f9341831812
     1.1 --- a/src/Pure/tactic.ML	Sun May 28 20:53:03 2006 +0200
     1.2 +++ b/src/Pure/tactic.ML	Mon May 29 13:15:53 2006 +0200
     1.3 @@ -133,10 +133,10 @@
     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 (zero_var_indexes rl)
     1.8 +  let val (st, thaw) = freeze_thaw_robust (zero_var_indexes rl)
     1.9    in case Seq.pull (tac st)  of
    1.10          NONE        => raise THM("rule_by_tactic", 0, [rl])
    1.11 -      | SOME(st',_) => Thm.varifyT (thaw st')
    1.12 +      | SOME(st',_) => Thm.varifyT (thaw 0 st')
    1.13    end;
    1.14  
    1.15  (*** Basic tactics ***)