src/ZF/AC/WO1_WO8.ML

 by (eres_inst_tac [("x","{{x}. x:A}")] allE 1);
 by (etac impE 1);
 by (fast_tac (!claset addSEs [lam_sing_bij RS bij_is_inj RS
                         well_ord_rvimage]) 2);
 by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1);
-by (fast_tac (!claset addSEs [singleton_eq_iff RS iffD1 RS sym]
-                addSIs [lam_type]
-                addIs [the_equality RS ssubst]) 1);
+by (fast_tac (!claset addSIs [lam_type]
+                addss (!simpset addsimps [singleton_eq_iff, the_equality])) 1);
 qed "WO8_WO1";