src/ZF/AC/DC.ML

--- a/src/ZF/AC/DC.ML	Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/AC/DC.ML	Thu Aug 06 10:38:57 1998 +0200
@@ -574,7 +574,7 @@
 Goal "[| ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y, x> : R);  \
 \        b:a; Z:Pow(X); Z lesspoll a |]  \
 \     ==> {x:X. <Z,x> : R} ~= 0";
-by (blast_tac (claset() addEs [equals0E]) 1);
+by (Blast_tac 1);
 val lemmaX = result();
 
 Goal "[| Card(K); well_ord(X,Q);  \