diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/HH.ML
--- a/src/ZF/AC/HH.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/HH.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -151,8 +151,7 @@
 qed "lam_surj_sing";
 
 Goal "y:Pow(x)-{0} ==> x ~= 0";
-by (fast_tac (claset() addSIs [equals0I, singletonI RS subst_elem]
-                addSDs [equals0D]) 1);
+by Auto_tac;
 qed "not_emptyI2";
 
 Goal "f`(x - (UN j:i. HH(f,x,j))): Pow(x - (UN j:i. HH(f,x,j)))-{0}  \