--- a/src/Pure/tactic.ML Sun May 28 20:53:03 2006 +0200
+++ b/src/Pure/tactic.ML Mon May 29 13:15:53 2006 +0200
@@ -133,10 +133,10 @@
(*Makes a rule by applying a tactic to an existing rule*)
fun rule_by_tactic tac rl =
- let val (st, thaw) = freeze_thaw (zero_var_indexes rl)
+ let val (st, thaw) = freeze_thaw_robust (zero_var_indexes rl)
in case Seq.pull (tac st) of
NONE => raise THM("rule_by_tactic", 0, [rl])
- | SOME(st',_) => Thm.varifyT (thaw st')
+ | SOME(st',_) => Thm.varifyT (thaw 0 st')
end;
(*** Basic tactics ***)