diff -r 9154d8410514 -r d4c6e2bdde59 src/ZF/Zorn.ML
--- a/src/ZF/Zorn.ML	Thu Sep 08 13:17:57 1994 +0200
+++ b/src/ZF/Zorn.ML	Fri Sep 09 11:40:40 1994 +0200
@@ -36,14 +36,6 @@
 by (assume_tac 1);
 val increasingD2 = result();
 
-(*????????????????????????????????????????????????????????????????
-goal Zorn.thy
-    "!!next S. [| X : Pow(S);  next: increasing(S) |] ==> next`X : Pow(S)";
-by (eresolve_tac [increasingD1 RS apply_type] 1);
-by (assume_tac 1);
-val next_bounded = result();
-*)
-
 (*Introduction rules*)
 val [TFin_nextI, Pow_TFin_UnionI] = TFin.intrs;
 val TFin_UnionI = PowI RS Pow_TFin_UnionI;