Modified proofs because simplifier does not eta-contract any longer.

--- a/src/HOL/MiniML/W.ML	Fri Mar 14 10:35:30 1997 +0100
+++ b/src/HOL/MiniML/W.ML	Fri Mar 14 10:37:01 1997 +0100
@@ -568,18 +568,19 @@
 by (case_tac "na: free_tv t - free_tv Sa" 2);
 (* case na ~: free_tv t - free_tv Sa *)
 by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
+by (Fast_tac 3);
 (* case na : free_tv t - free_tv Sa *)
 by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
 by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
 by (dtac eq_subst_scheme_list_eq_free 2);
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
+(** LEVEL 75 **)
 by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
-
 by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); 
 by (safe_tac HOL_cs );
 by (dtac mgu_Some 1);
 by( fast_tac (HOL_cs addss !simpset) 1);
-
+(** LEVEL 80 *)
 by ((dtac mgu_mg 1) THEN (atac 1));
 by (etac exE 1);
 by (res_inst_tac [("x","Rb")] exI 1);
@@ -588,8 +589,8 @@
 by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
 by (simp_tac (!simpset addsimps [subst_comp_scheme_list]) 1);
 by (simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym]) 1);
-by (res_inst_tac [("A2","($ Sa ($ S A))")] ((subst_comp_scheme_list RS sym) RSN 
-    (2,trans)) 1);
+by (res_inst_tac [("A2","($ Sa ($ S A))")]
+       ((subst_comp_scheme_list RS sym) RSN (2,trans)) 1);
 by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
 by (rtac eq_free_eq_subst_scheme_list 1);
 by( safe_tac HOL_cs );
@@ -598,10 +599,10 @@
 by (etac conjE 2);
 by (dtac new_tv_subst_scheme_list 2);
 by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 2);
-by (( forw_inst_tac [("n","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));
+by (forw_inst_tac [("n","m")] new_tv_W 2  THEN  atac 2);
 by (etac conjE 2);
 by (dtac (free_tv_app_subst_scheme_list RS subsetD) 2);
-by (fast_tac (set_cs addDs [W_var_geD,new_scheme_list_le,codD,
+by (fast_tac (set_cs addDs [sym RS W_var_geD,new_scheme_list_le,codD,
     new_tv_not_free_tv]) 2);
 by (case_tac "na: free_tv t - free_tv Sa" 1);
 (* case na ~: free_tv t - free_tv Sa *)

--- a/src/HOL/W0/I.ML	Fri Mar 14 10:35:30 1997 +0100
+++ b/src/HOL/W0/I.ML	Fri Mar 14 10:37:01 1997 +0100
@@ -103,8 +103,6 @@
      [asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te]),
       REPEAT o etac conjE, hyp_subst_tac]));
 (** LEVEL 70 **)
-by (safe_tac HOL_cs);
- by (simp_tac (!simpset addsimps [o_def,subst_comp_te]) 2);
 by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1);
  by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
@@ -114,14 +112,14 @@
                        addss !simpset) 1);
  by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
                       addss !simpset) 1);
-(** LEVEL 79 **)
+(** LEVEL 77 **)
 by (dres_inst_tac [("e","expr1")] (sym RS W_var_geD) 1);
 by ((dtac new_tv_subst_tel 1) THEN (atac 1));
 by ((dres_inst_tac [("ts","$ s a")] new_tv_list_le 1) THEN (atac 1));
 by ((dtac new_tv_subst_tel 1) THEN (atac 1));
 by (best_tac (HOL_cs addDs [new_tv_W] 
                      addss (!simpset addsimps [subst_comp_tel])) 1);
-(** LEVEL 84 **)
+(** LEVEL 82 **)
 qed_spec_mp "I_correct_wrt_W";
 
 (***

--- a/src/HOL/W0/W.ML	Fri Mar 14 10:35:30 1997 +0100
+++ b/src/HOL/W0/W.ML	Fri Mar 14 10:37:01 1997 +0100
@@ -19,8 +19,8 @@
 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
                         setloop (split_tac [expand_bind])) 1);
 by (strip_tac 1);
-by (eres_inst_tac [("x","TVar(n) # a")] allE 1);
-by ( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1);
+bd sym 1;
+by (fast_tac (HOL_cs addss !simpset) 1);
 (* case App e1 e2 *)
 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
 by (strip_tac 1);
@@ -91,10 +91,9 @@
 \                 new_tv m s & new_tv m t";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
-by (fast_tac (HOL_cs unsafe_addss (!simpset 
-        addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] 
+by (fast_tac (HOL_cs addDs [list_all_nth] unsafe_addss (!simpset 
+        addsimps [id_subst_def,new_tv_list,new_tv_subst] 
         setloop (split_tac [expand_if]))) 1);
-
 (* case Abs e *)
 by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 
     setloop (split_tac [expand_bind])) 1);
@@ -288,8 +287,8 @@
 (** LEVEL 42 **)
 by (case_tac "na:free_tv sa" 2);
 (* na ~: free_tv sa *)
-by (asm_simp_tac (!simpset addsimps [not_free_impl_id]
-                  setloop (split_tac [expand_if])) 3);
+by (forward_tac [not_free_impl_id] 3);
+by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
 (* na : free_tv sa *)
 by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
 by (dtac eq_subst_tel_eq_free 2);
@@ -297,9 +296,9 @@
 by (Asm_simp_tac 2); 
 by (case_tac "na:dom sa" 2);
 (* na ~: dom sa *)
+(** LEVEL 50 **)
 by (asm_full_simp_tac (!simpset addsimps [dom_def] 
                        setloop (split_tac [expand_if])) 3);
-(** LEVEL 50 **)
 (* na : dom sa *)
 by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2);
@@ -313,8 +312,8 @@
 by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
                             setloop (split_tac [expand_if]))) 2);
 
+(** LEVEL 60 **)
 by (Simp_tac 2);  
-(** LEVEL 60 **)
 by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2 );
 by (subgoal_tac "na ~= ma" 2);
@@ -323,7 +322,7 @@
 by (dtac (sym RS W_var_geD) 3);
 by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3);
 by (case_tac "na: free_tv t - free_tv sa" 2);
-(** LEVEL 68 **)
+(** LEVEL 69 **)
 (* case na ~: free_tv t - free_tv sa *)
 by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
 (* case na : free_tv t - free_tv sa *)
@@ -331,10 +330,11 @@
 by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
 by (dtac eq_subst_tel_eq_free 2);
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
-by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 2);
-(** LEVEL 74 **)
-by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 
-by (safe_tac HOL_cs );
+by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
+by (Fast_tac 2);
+(** LEVEL 76 **)
+by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (safe_tac HOL_cs);
 by (dtac mgu_Ok 1);
 by ( fast_tac (HOL_cs addss !simpset) 1);
 by (REPEAT (resolve_tac [exI,conjI] 1));
@@ -347,9 +347,9 @@
 by (dres_inst_tac [("x","ma")] fun_cong 2);
 by ( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
 by (simp_tac (!simpset addsimps [o_def,subst_comp_tel RS sym]) 1);
+(** LEVEL 90 **)
 by (rtac ((subst_comp_tel RS sym) RSN (2,trans)) 1);
 by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
-(** LEVEL 90 **)
 by (rtac eq_free_eq_subst_tel 1);
 by ( safe_tac HOL_cs );
 by (subgoal_tac "ma ~= na" 1);
@@ -357,11 +357,11 @@
 by (etac conjE 2);
 by (dtac new_tv_subst_tel 2);
 by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2);
-by (( forw_inst_tac [("n","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));
+by (forw_inst_tac [("n","m")] new_tv_W 2 THEN atac 2);
+(** LEVEL 100 **)
 by (etac conjE 2);
 by (dtac (free_tv_app_subst_tel RS subsetD) 2);
-(** LEVEL 100 **)
-by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD,
+by (fast_tac (set_cs addDs [sym RS W_var_geD,new_tv_list_le,codD,
     new_tv_not_free_tv]) 2);
 by (case_tac "na: free_tv t - free_tv sa" 1);
 (* case na ~: free_tv t - free_tv sa *)
@@ -371,7 +371,7 @@
 by (dtac (free_tv_app_subst_tel RS subsetD) 1);
 by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
 			    eq_subst_tel_eq_free] 
-       addss ((!simpset addsimps [de_Morgan_disj,free_tv_subst,dom_def]))) 1);
+       addss ((!simpset addsimps [free_tv_subst,dom_def]))) 1);
 (** LEVEL 106 **)
 by (Fast_tac 1);
 qed_spec_mp "W_complete_lemma";