# HG changeset patch
# User paulson
# Date 857141201 -3600
# Node ID 889a1cbd1aca7ea6332c47d81f421506af321482
# Parent  b7c86d3c9d0a2c0dd441f15c76944843120cbffe
rule_by_tactic no longer standardizes its result

diff -r b7c86d3c9d0a -r 889a1cbd1aca src/HOL/intr_elim.ML
--- a/src/HOL/intr_elim.ML	Fri Feb 28 15:44:32 1997 +0100
+++ b/src/HOL/intr_elim.ML	Fri Feb 28 15:46:41 1997 +0100
@@ -144,7 +144,8 @@
   (*String s should have the form t:Si where Si is an inductive set*)
   fun mk_cases defs s = 
       rule_by_tactic (con_elim_tac defs)
-        (assume_read Inductive.thy s  RS  elim);
+          (assume_read Inductive.thy s  RS  elim) 
+      |> standard;
 
   val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct)
   and rec_names = rec_names
diff -r b7c86d3c9d0a -r 889a1cbd1aca src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Feb 28 15:44:32 1997 +0100
+++ b/src/Pure/tactic.ML	Fri Feb 28 15:46:41 1997 +0100
@@ -106,10 +106,11 @@
 in
   fun freeze_thaw th =
     let val fth = freezeT th
+	val vary = variant (add_term_names (#prop(rep_thm fth), []))
 	val {prop,sign,...} = rep_thm fth
 	fun mk_inst (Var(v,T)) = 
 	    (cterm_of sign (Var(v,T)),
-	     cterm_of sign (Free(string_of v, T)))
+	     cterm_of sign (Free(vary (string_of v), T)))
 	val insts = map mk_inst (term_vars prop)
 	fun thaw th' = 
 	    th' |> forall_intr_list (map #2 insts)
@@ -135,9 +136,11 @@
 
 (*Makes a rule by applying a tactic to an existing rule*)
 fun rule_by_tactic tac rl =
-    case rl |> standard |> freeze_thaw |> #1 |> tac |> Sequence.pull of
+  let val (st, thaw) = freeze_thaw (zero_var_indexes rl)
+  in case Sequence.pull (tac st)  of
 	None        => raise THM("rule_by_tactic", 0, [rl])
-      | Some(rl',_) => standard rl';
+      | Some(st',_) => Thm.varifyT (thaw st')
+  end;
  
 (*** Basic tactics ***)
 
diff -r b7c86d3c9d0a -r 889a1cbd1aca src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Fri Feb 28 15:44:32 1997 +0100
+++ b/src/ZF/Perm.ML	Fri Feb 28 15:46:41 1997 +0100
@@ -238,10 +238,10 @@
 by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
 qed "compE";
 
-val compEpair = 
+bind_thm ("compEpair", 
     rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)
                     THEN prune_params_tac)
-        (read_instantiate [("xz","<a,c>")] compE);
+        (read_instantiate [("xz","<a,c>")] compE));
 
 AddSIs [idI];
 AddIs  [compI];
diff -r b7c86d3c9d0a -r 889a1cbd1aca src/ZF/intr_elim.ML
--- a/src/ZF/intr_elim.ML	Fri Feb 28 15:44:32 1997 +0100
+++ b/src/ZF/intr_elim.ML	Fri Feb 28 15:46:41 1997 +0100
@@ -155,7 +155,8 @@
       rule_by_tactic (rewrite_goals_tac defs THEN 
                       basic_elim_tac THEN
                       fold_tac defs)
-        (assume_read Inductive.thy s  RS  elim);
+         (assume_read Inductive.thy s  RS  elim)
+      |> standard;
 
   val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
   and rec_names = rec_names