diff -r 024d887eae50 -r 855654b691db src/ZF/AC/AC7_AC9.ML
--- a/src/ZF/AC/AC7_AC9.ML	Thu Sep 10 17:42:02 1998 +0200
+++ b/src/ZF/AC/AC7_AC9.ML	Thu Sep 10 17:42:44 1998 +0200
@@ -91,8 +91,7 @@
 val lemma1_2 = result();
 
 Goal "(PROD B:{(nat->Union(A))*C. C:A}. B) ~= 0 ==> (PROD B:A. B) ~= 0";
-by (fast_tac (claset() addSIs [equals0I,lemma1_1, lemma1_2]
-                addSEs [equals0E]) 1);
+by (fast_tac (claset() addSIs [equals0I,lemma1_1, lemma1_2]) 1);
 val lemma1 = result();
 
 Goal "0 ~: A ==> 0 ~: {(nat -> Union(A)) * C. C:A}";