# HG changeset patch
# User paulson
# Date 963486140 -7200
# Node ID f1ad1ed0d110567441c81ae4b6e8f1ed6c72d8a1
# Parent  8adf653d40a1157750fa387b944b253681c3f29f
fixed a failing proof

diff -r 8adf653d40a1 -r f1ad1ed0d110 src/ZF/equalities.ML
--- 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 **)