# HG changeset patch
# User wenzelm
# Date 1129911272 -7200
# Node ID 3b34516662c642302c0de4744939bcce59a88c51
# Parent  42fc2ac69c8cfbc3b4031436b956a2bf52569b9d
avoid shortcuts from OldGoals;

diff -r 42fc2ac69c8c -r 3b34516662c6 src/CCL/Fix.ML
--- a/src/CCL/Fix.ML	Fri Oct 21 16:34:22 2005 +0200
+++ b/src/CCL/Fix.ML	Fri Oct 21 18:14:32 2005 +0200
@@ -182,7 +182,7 @@
 by (REPEAT_SOME (ares_tac [allI]));
 by (stac applyBbot 1);
 by (resolve_tac prems 1);
-br (applyB RS ssubst )1;
+by (rtac (applyB RS ssubst) 1);
 by (res_inst_tac [("t","xa")] term_case 1);
 by (ALLGOALS (simp_tac term_ss));
 by (ALLGOALS (fast_tac (term_cs addIs ([all_INCL,INCL_subst] @ prems))));
diff -r 42fc2ac69c8c -r 3b34516662c6 src/HOLCF/FOCUS/Stream_adm.ML
--- a/src/HOLCF/FOCUS/Stream_adm.ML	Fri Oct 21 16:34:22 2005 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.ML	Fri Oct 21 18:14:32 2005 +0200
@@ -84,7 +84,7 @@
 Goal "[| !i. ? l. !x y. \
 \Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;\
 \   down_cont F |] ==> adm (%x. x:gfp F)";
-byev[   etac (INTER_down_iterate_is_gfp RS ssubst) 1, (* cont *)
+by (EVERY [   etac (INTER_down_iterate_is_gfp RS ssubst) 1, (* cont *)
         Simp_tac 1,
         resolve_tac adm_lemmas 1,
         rtac flatstream_admI 1,
@@ -99,7 +99,7 @@
          atac 1,
         dtac mp 1,
          etac is_ub_thelub 1,
-        Fast_tac 1];
+        Fast_tac 1]);
 qed "stream_monoP2_gfp_admI";
 
 bind_thm("fstream_gfp_admI",stream_monoP2I RS stream_monoP2_gfp_admI);
diff -r 42fc2ac69c8c -r 3b34516662c6 src/HOLCF/IOA/meta_theory/CompoExecs.ML
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Fri Oct 21 16:34:22 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Fri Oct 21 18:14:32 2005 +0200
@@ -161,7 +161,7 @@
 
 by (pair_induct_tac "xs" [is_exec_frag_def] 1);
 (* main case *)
-ren "ss a t" 1;
+by (rename_tac "ss a t" 1);
 by (safe_tac set_cs);
 by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));
 qed"lemma_1_1a";
diff -r 42fc2ac69c8c -r 3b34516662c6 src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Fri Oct 21 16:34:22 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Fri Oct 21 18:14:32 2005 +0200
@@ -472,7 +472,7 @@
 
 (* mkex is exactly the construction of exA||B out of exA, exB, and the oracle sch,
    we need here *)
-ren "exA exB" 1;
+by (rename_tac "exA exB" 1);
 by (res_inst_tac [("x","mkex A B sch exA exB")] bexI 1);
 (* mkex actions are just the oracle *)
 by (pair_tac "exA" 1);
diff -r 42fc2ac69c8c -r 3b34516662c6 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Fri Oct 21 16:34:22 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Fri Oct 21 18:14:32 2005 +0200
@@ -690,7 +690,7 @@
 by (thin_tac' 5 1);
 by (rtac nat_less_induct 1);
 by (REPEAT (rtac allI 1));
-ren "tr schB schA" 1;
+by (rename_tac "tr schB schA" 1);
 by (strip_tac 1);
 by (REPEAT (etac conjE 1));
 
@@ -930,7 +930,7 @@
 by (thin_tac' 5 1);
 by (rtac nat_less_induct 1);
 by (REPEAT (rtac allI 1));
-ren "tr schB schA" 1;
+by (rename_tac "tr schB schA" 1);
 by (strip_tac 1);
 by (REPEAT (etac conjE 1));
 
@@ -1188,7 +1188,7 @@
 by (dtac scheds_in_sig 1);
 by (assume_tac 1);
 
-ren "h1 h2 schA schB" 1;
+by (rename_tac "h1 h2 schA schB" 1);
 (* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
    we need here *)
 by (res_inst_tac [("x","mksch A B$tr$schA$schB")] bexI 1);
diff -r 42fc2ac69c8c -r 3b34516662c6 src/HOLCF/IOA/meta_theory/Deadlock.ML
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Fri Oct 21 16:34:22 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Fri Oct 21 18:14:32 2005 +0200
@@ -14,7 +14,7 @@
 by (ftac inp_is_act 1);
 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
 by (pair_tac "ex" 1);
-ren "s ex" 1;
+by (rename_tac "s ex" 1);
 by (subgoal_tac "Finite ex" 1);
 by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 2);
 by (rtac (Map2Finite RS iffD1) 2);
diff -r 42fc2ac69c8c -r 3b34516662c6 src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Fri Oct 21 16:34:22 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Fri Oct 21 18:14:32 2005 +0200
@@ -155,7 +155,7 @@
 by (res_inst_tac [("x","s")] spec 1);
 by (rtac nat_less_induct 1);
 by (strip_tac 1);
-ren "na n s" 1;
+by (rename_tac "na n s" 1);
 by (case_tac "Forall (%x. ~ P x) s" 1);
 by (rtac (take_lemma_less RS iffD2 RS spec) 1);
 by (asm_full_simp_tac (simpset() addsimps [Cut_UU]) 1);
diff -r 42fc2ac69c8c -r 3b34516662c6 src/HOLCF/IOA/meta_theory/SimCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Fri Oct 21 16:34:22 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Fri Oct 21 18:14:32 2005 +0200
@@ -160,7 +160,7 @@
 by (pair_induct_tac "ex" [is_exec_frag_def] 1);
 (* cons case *)
 by (safe_tac set_cs);
-ren "ex a t s s'" 1;
+by (rename_tac "ex a t s s'" 1);
 by (asm_full_simp_tac (simpset() addsimps [mk_traceConc]) 1);
 by (forward_tac [reachable.reachable_n] 1);
 by (assume_tac 1);
@@ -191,7 +191,7 @@
 by (pair_induct_tac "ex" [is_exec_frag_def] 1);
 (* main case *)
 by (safe_tac set_cs);
-ren "ex a t s s'" 1;
+by (rename_tac "ex a t s s'" 1);
 by (res_inst_tac [("t",
                    "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")]
     lemma_2_1 1);
@@ -265,7 +265,7 @@
 
   (* Traces coincide, Lemma 1 *)
   by (pair_tac "ex" 1);
-  ren "s ex" 1;
+  by (rename_tac "s ex" 1);
   by (simp_tac (simpset() addsimps [corresp_ex_sim_def]) 1);
   by (res_inst_tac [("s","s")] traces_coincide_sim 1);
   by (REPEAT (atac 1));
@@ -275,7 +275,7 @@
   (* corresp_ex_sim is execution, Lemma 2 *)
   by (pair_tac "ex" 1);
   by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
-  ren "s ex" 1;
+  by (rename_tac "s ex" 1);
 
   (* start state *)
   by (rtac conjI 1);
diff -r 42fc2ac69c8c -r 3b34516662c6 src/HOLCF/IOA/meta_theory/Traces.ML
--- a/src/HOLCF/IOA/meta_theory/Traces.ML	Fri Oct 21 16:34:22 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Fri Oct 21 18:14:32 2005 +0200
@@ -198,7 +198,7 @@
 
 by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
 (* main case *)
-ren "ss a t" 1;
+by (rename_tac "ss a t" 1);
 by (safe_tac set_cs);
 by (REPEAT (asm_full_simp_tac (simpset() addsimps [is_trans_of_def]) 1));
 qed"execfrag_in_sig";