fixed a failing proof

--- a/src/ZF/equalities.ML	Thu Jul 13 13:00:22 2000 +0200
+++ b/src/ZF/equalities.ML	Thu Jul 13 13:02:20 2000 +0200
@@ -601,8 +601,7 @@
 (** RepFun **)
 
 Goal "{f(x).x:A}=0 <-> A=0";
-	(*blast_tac takes too long to find a good depth*)
-by (Blast.depth_tac (claset() addSEs [equalityE]) 10 1);
+by (Blast_tac 1);
 qed "RepFun_eq_0_iff";
 
 (** Collect **)