# HG changeset patch
# User paulson
# Date 857726471 -3600
# Node ID 2f477a0e690d35ed9e35c4daa074422feb55a292
# Parent  3ae9ccdd701e5174cb47ff637b3bbd65a48d95bf
Deleted steps made redundant by the stronger eq_assume_tac

diff -r 3ae9ccdd701e -r 2f477a0e690d src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Fri Mar 07 10:20:26 1997 +0100
+++ b/src/HOL/MiniML/W.ML	Fri Mar 07 10:21:11 1997 +0100
@@ -484,7 +484,7 @@
 by (Asm_simp_tac 1);
 by (asm_simp_tac (!simpset addsimps [(bound_typ_inst_composed_subst RS sym),new_tv_nth_nat_A,o_def,nth_subst] 
                            delsimps [bound_typ_inst_composed_subst]) 1);
-
+(** LEVEL 12 **)
 (* case Abs e *)
 by (strip_tac 1);
 by (eresolve_tac has_type_casesE 1);
@@ -492,8 +492,10 @@
 by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
 by (eres_inst_tac [("x","t2")] allE 1);
 by (eres_inst_tac [("x","Suc n")] allE 1);
-by (best_tac (HOL_cs addSDs [mk_scheme_injective] unsafe_addss (!simpset addcongs [conj_cong] 
-    setloop (split_tac [expand_option_bind]))) 1);
+by (best_tac (HOL_cs addSDs [mk_scheme_injective] 
+                  unsafe_addss (!simpset addcongs [conj_cong] 
+				setloop (split_tac [expand_option_bind]))) 1);
+(** LEVEL 19 **)
 
 (* case App e1 e2 *)
 by (strip_tac 1);
@@ -503,16 +505,14 @@
 by (eres_inst_tac [("x","t2 -> t'")] allE 1);
 by (eres_inst_tac [("x","n")] allE 1);
 by (safe_tac HOL_cs);
+(** LEVEL 26 **)
 by (eres_inst_tac [("x","R")] allE 1);
 by (eres_inst_tac [("x","$ S A")] allE 1);
 by (eres_inst_tac [("x","t2")] allE 1);
 by (eres_inst_tac [("x","m")] allE 1);
-by (dtac asm_rl 1);
-by (dtac asm_rl 1);
-by (dtac asm_rl 1);
+by (rotate_tac ~3 1);
 by (Asm_full_simp_tac 1);
 by (safe_tac HOL_cs);
-by (fast_tac HOL_cs 1);
 by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
         conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1);
 
@@ -528,7 +528,7 @@
 by (rtac eq_free_eq_subst_te 2);  
 by (strip_tac 2);
 by (subgoal_tac "na ~=ma" 2);
-by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
+by (best_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
     new_tv_not_free_tv,new_tv_le]) 3);
 by (case_tac "na:free_tv Sa" 2);
 (* n1 ~: free_tv S1 *)
diff -r 3ae9ccdd701e -r 2f477a0e690d src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Fri Mar 07 10:20:26 1997 +0100
+++ b/src/HOLCF/Fix.ML	Fri Mar 07 10:21:11 1997 +0100
@@ -1100,7 +1100,6 @@
  (fn prems =>
         [
         safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
-        atac 2,
         asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1,
         res_inst_tac [("x","i")] exI 1,
         strip_tac 1,