src/ZF/equalities.ML

--- a/src/ZF/equalities.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/equalities.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -532,8 +532,8 @@
 (** RepFun **)
 
 goal ZF.thy "{f(x).x:A}=0 <-> A=0";
-	(*blast_tac takes too long to search depth 5*)
-by (Blast.depth_tac (!claset addSEs [equalityE]) 6 1);
+	(*blast_tac takes too long to find a good depth*)
+by (Blast.depth_tac (!claset addSEs [equalityE]) 10 1);
 qed "RepFun_eq_0_iff";
 
 (** Collect **)