src/ZF/AC/AC_Equiv.ML

--- a/src/ZF/AC/AC_Equiv.ML	Thu Sep 10 17:42:02 1998 +0200
+++ b/src/ZF/AC/AC_Equiv.ML	Thu Sep 10 17:42:44 1998 +0200
@@ -39,7 +39,7 @@
 (* ********************************************************************** *)
 
 Goal "(A->X)=0 ==> X=0";
-by (fast_tac (claset() addSIs [equals0I] addEs [lam_type RSN (2, equals0E)]) 1);
+by (fast_tac (claset() addSIs [equals0I] addIs [lam_type]) 1);
 qed "fun_space_emptyD";
 
 (* used only in WO1_DC.ML *)