src/ZF/AC/AC_Equiv.ML

--- a/src/ZF/AC/AC_Equiv.ML	Fri Sep 18 15:09:26 1998 +0200
+++ b/src/ZF/AC/AC_Equiv.ML	Fri Sep 18 15:09:46 1998 +0200
@@ -95,8 +95,7 @@
 qed "Inf_Card_is_InfCard";
 
 Goal "(THE z. {x}={z}) = x";
-by (fast_tac (claset() addSIs [the_equality]
-                addSEs [singleton_eq_iff RS iffD1 RS sym]) 1);
+by (fast_tac (claset() addSEs [singleton_eq_iff RS iffD1 RS sym]) 1);
 qed "the_element";
 
 Goal "(lam x:A. {x}) : bij(A, {{x}. x:A})";