--- a/src/HOL/Real/Hyperreal/Zorn.ML Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.ML Mon Aug 16 18:41:32 1999 +0200
@@ -1,11 +1,10 @@
(* Title : Zorn.ML
+ ID : $Id$
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Description : Zorn's Lemma -- adapted proofs from lcp's ZF/Zorn.ML
*)
-open Zorn;
-
(*---------------------------------------------------------------
Section 1. Mathematical Preamble
---------------------------------------------------------------*)