diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/AC/AC16_WO4.ML
--- a/src/ZF/AC/AC16_WO4.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/AC/AC16_WO4.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -328,11 +328,10 @@
 by (res_inst_tac 
      [("f3", "lam b:y-a. THE c. c: s(u) & a <= c & b:c")]
      (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
-by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
-by (rtac CollectI 1);
+by (simp_tac (simpset() addsimps [inj_def]) 1);
+by (rtac conjI 1);
 by (rtac lam_type 1);
-by (forward_tac [ex1_superset_a RS theI] 1
-        THEN REPEAT (Fast_tac 1));
+by (forward_tac [ex1_superset_a RS theI] 1 THEN REPEAT (Fast_tac 1));
 by (Asm_simp_tac 1);
 by (Clarify_tac 1);
 by (rtac cons_eqE 1);
@@ -387,17 +386,16 @@
 \     ==> {v:s(u). a <= v} lepoll {v:Pow(x). v eqpoll m}";
 by (res_inst_tac [("f3","lam w:{v:s(u). a <= v}. w Int (x - {u})")] 
         (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
-by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
-by (rtac CollectI 1);
+by (simp_tac (simpset() addsimps [inj_def]) 1);
+by (rtac conjI 1);
 by (rtac lam_type 1);
 by (rtac CollectI 1);
 by (Fast_tac 1);
 by (rtac w_Int_eqpoll_m 1 THEN REPEAT (assume_tac 1));
-by (simp_tac (simpset() delsimps ball_simps) 1);
 by (REPEAT (resolve_tac [ballI, impI] 1));
-(** LEVEL 9 **)
-by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1
-        THEN REPEAT (assume_tac 1));
+(** LEVEL 8 **)
+by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1);
+by (EVERY (map Blast_tac [4,3,2,1]));
 by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1));
 by (forward_tac [cons_cons_in] 1 THEN REPEAT (assume_tac 1));
 by (etac ex1_two_eq 1);