# 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 **)