--- a/src/HOL/Real/Hyperreal/Zorn.thy Tue Sep 21 17:29:46 1999 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.thy Tue Sep 21 17:30:11 1999 +0200
@@ -5,7 +5,7 @@
Description : Zorn's Lemma -- See lcp's Zorn.thy in ZF
*)
-Zorn = Finite +
+Zorn = Main +
constdefs
chain :: 'a set => 'a set set