src/ZF/AC/AC7_AC9.ML

--- a/src/ZF/AC/AC7_AC9.ML	Tue Mar 10 14:27:44 1998 +0100
+++ b/src/ZF/AC/AC7_AC9.ML	Tue Mar 10 16:47:26 1998 +0100
@@ -140,7 +140,6 @@
 by (REPEAT (eresolve_tac [exE,conjE] 1));
 by (hyp_subst_tac 1);
 by (Asm_full_simp_tac 1);
-by (fast_tac (claset() addSEs [sym RS equals0D]) 1);
 val lemma1 = result();
 
 goal thy "!!A. [| f: (PROD X:RepFun(A,p). X); D:A |]  \