--- a/src/HOL/Real/Hyperreal/Zorn.ML Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/Hyperreal/Zorn.ML Wed May 10 22:34:30 2000 +0200 @@ -289,4 +289,3 @@ Goal "x : Union(c) ==> EX m:c. x:m"; by (Blast_tac 1); qed "mem_UnionD"; -