src/ZF/AC/WO1_WO8.ML

--- a/src/ZF/AC/WO1_WO8.ML	Mon Aug 19 15:35:11 1996 +0200
+++ b/src/ZF/AC/WO1_WO8.ML	Tue Aug 20 12:23:13 1996 +0200
@@ -25,6 +25,6 @@
                         well_ord_rvimage]) 2);
 by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1);
 by (fast_tac (ZF_cs addSEs [RepFunE, singleton_eq_iff RS iffD1 RS sym]
-                addSIs [lam_type, singletonI]
+                addSIs [lam_type]
                 addIs [the_equality RS ssubst]) 1);
 qed "WO8_WO1";