rule_by_tactic no longer standardizes its result
authorpaulson
Fri Feb 28 15:46:41 1997 +0100 (1997-02-28)
changeset 2688889a1cbd1aca
parent 2687 b7c86d3c9d0a
child 2689 6d3d893453de
rule_by_tactic no longer standardizes its result
src/HOL/intr_elim.ML
src/Pure/tactic.ML
src/ZF/Perm.ML
src/ZF/intr_elim.ML
     1.1 --- a/src/HOL/intr_elim.ML	Fri Feb 28 15:44:32 1997 +0100
     1.2 +++ b/src/HOL/intr_elim.ML	Fri Feb 28 15:46:41 1997 +0100
     1.3 @@ -144,7 +144,8 @@
     1.4    (*String s should have the form t:Si where Si is an inductive set*)
     1.5    fun mk_cases defs s = 
     1.6        rule_by_tactic (con_elim_tac defs)
     1.7 -        (assume_read Inductive.thy s  RS  elim);
     1.8 +          (assume_read Inductive.thy s  RS  elim) 
     1.9 +      |> standard;
    1.10  
    1.11    val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct)
    1.12    and rec_names = rec_names
     2.1 --- a/src/Pure/tactic.ML	Fri Feb 28 15:44:32 1997 +0100
     2.2 +++ b/src/Pure/tactic.ML	Fri Feb 28 15:46:41 1997 +0100
     2.3 @@ -106,10 +106,11 @@
     2.4  in
     2.5    fun freeze_thaw th =
     2.6      let val fth = freezeT th
     2.7 +	val vary = variant (add_term_names (#prop(rep_thm fth), []))
     2.8  	val {prop,sign,...} = rep_thm fth
     2.9  	fun mk_inst (Var(v,T)) = 
    2.10  	    (cterm_of sign (Var(v,T)),
    2.11 -	     cterm_of sign (Free(string_of v, T)))
    2.12 +	     cterm_of sign (Free(vary (string_of v), T)))
    2.13  	val insts = map mk_inst (term_vars prop)
    2.14  	fun thaw th' = 
    2.15  	    th' |> forall_intr_list (map #2 insts)
    2.16 @@ -135,9 +136,11 @@
    2.17  
    2.18  (*Makes a rule by applying a tactic to an existing rule*)
    2.19  fun rule_by_tactic tac rl =
    2.20 -    case rl |> standard |> freeze_thaw |> #1 |> tac |> Sequence.pull of
    2.21 +  let val (st, thaw) = freeze_thaw (zero_var_indexes rl)
    2.22 +  in case Sequence.pull (tac st)  of
    2.23  	None        => raise THM("rule_by_tactic", 0, [rl])
    2.24 -      | Some(rl',_) => standard rl';
    2.25 +      | Some(st',_) => Thm.varifyT (thaw st')
    2.26 +  end;
    2.27   
    2.28  (*** Basic tactics ***)
    2.29  
     3.1 --- a/src/ZF/Perm.ML	Fri Feb 28 15:44:32 1997 +0100
     3.2 +++ b/src/ZF/Perm.ML	Fri Feb 28 15:46:41 1997 +0100
     3.3 @@ -238,10 +238,10 @@
     3.4  by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
     3.5  qed "compE";
     3.6  
     3.7 -val compEpair = 
     3.8 +bind_thm ("compEpair", 
     3.9      rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)
    3.10                      THEN prune_params_tac)
    3.11 -        (read_instantiate [("xz","<a,c>")] compE);
    3.12 +        (read_instantiate [("xz","<a,c>")] compE));
    3.13  
    3.14  AddSIs [idI];
    3.15  AddIs  [compI];
     4.1 --- a/src/ZF/intr_elim.ML	Fri Feb 28 15:44:32 1997 +0100
     4.2 +++ b/src/ZF/intr_elim.ML	Fri Feb 28 15:46:41 1997 +0100
     4.3 @@ -155,7 +155,8 @@
     4.4        rule_by_tactic (rewrite_goals_tac defs THEN 
     4.5                        basic_elim_tac THEN
     4.6                        fold_tac defs)
     4.7 -        (assume_read Inductive.thy s  RS  elim);
     4.8 +         (assume_read Inductive.thy s  RS  elim)
     4.9 +      |> standard;
    4.10  
    4.11    val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
    4.12    and rec_names = rec_names