# HG changeset patch
# User paulson
# Date 1148901353 -7200
# Node ID 0843210d3756863267edc15caaabda490c512ce4
# Parent  86f21beabafc9b979d36beae6680fcef83f4d30b
fixing a variable-clash bug in rule_by_tactic

diff -r 86f21beabafc -r 0843210d3756 src/Pure/tactic.ML
--- 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 ***)