# HG changeset patch
# User nipkow
# Date 889557868 -3600
# Node ID b820f57a2323f4cd0b566b5b53d3dde9368a2486
# Parent  6b7027b9e3f405c86c44ed49dc0a2c0a138e8756
Mod because of new simplifier.

diff -r 6b7027b9e3f4 -r b820f57a2323 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Tue Mar 10 20:24:04 1998 +0100
+++ b/src/HOL/MiniML/W.ML	Tue Mar 10 20:24:28 1998 +0100
@@ -46,26 +46,21 @@
 
 goal thy "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
 by (type_scheme.induct_tac "sch" 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
+  by (Asm_full_simp_tac 1);
+ by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
 by (strip_tac 1);
 by (Asm_full_simp_tac 1);
 by (etac conjE 1);
 by (rtac conjI 1);
+ by (rtac new_tv_le 1);
+  by (assume_tac 2);
+ by (rtac add_le_mono 1);
+  by (Simp_tac 1);
+ by (simp_tac (simpset() addsimps [max_def]) 1);
 by (rtac new_tv_le 1);
-by (mp_tac 2);
-by (mp_tac 2);
-by (assume_tac 2);
+ by (assume_tac 2);
 by (rtac add_le_mono 1);
-by (Simp_tac 1);
-by (simp_tac (simpset() addsimps [max_def]) 1);
-by (strip_tac 1);
-by (rtac new_tv_le 1);
-by (mp_tac 2);
-by (mp_tac 2);
-by (assume_tac 2);
-by (rtac add_le_mono 1);
-by (Simp_tac 1);
+ by (Simp_tac 1);
 by (simp_tac (simpset() addsimps [max_def]) 1);
 by (strip_tac 1);
 by (dtac not_leE 1);
@@ -433,10 +428,8 @@
 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 (rotate_tac ~3 1);
 by (Asm_full_simp_tac 1);
 by (safe_tac HOL_cs);
-by (contr_tac 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);
 (** LEVEL 35 **)
@@ -548,7 +541,6 @@
 by (eres_inst_tac [("x","gen ($ S A) t # $ S A")] allE 1);
 by (eres_inst_tac [("x","t'")] allE 1);
 by (eres_inst_tac [("x","m")] allE 1);
-by (rotate_tac 4 1);
 by (Asm_full_simp_tac 1);
 by (dtac mp 1);
 by (rtac has_type_le_env 1);