src/ZF/AC/AC17_AC1.ML

--- a/src/ZF/AC/AC17_AC1.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/AC17_AC1.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -61,8 +61,7 @@
 
 Goal "[| f`Z : Z; Z:Pow(x)-{0} |] ==>  \
 \       (lam X:Pow(x)-{0}. {f`X})`Z : Pow(Z)-{0}";
-by (Asm_full_simp_tac 1);
-by (fast_tac (claset() addSDs [equals0D]) 1);
+by Auto_tac;
 val lemma3 = result();
 
 Goal "EX f:F. f`((lam f:F. Q(f))`f) : (lam f:F. Q(f))`f  \