diff -r f174f3be058f -r bacf85370ce0 src/ZF/QUniv.ML
--- a/src/ZF/QUniv.ML	Fri Nov 06 15:48:37 1998 +0100
+++ b/src/ZF/QUniv.ML	Mon Nov 09 10:58:49 1998 +0100
@@ -3,11 +3,9 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-For quniv.thy.  A small universe for lazy recursive types
+A small universe for lazy recursive types
 *)
 
-open QUniv;
-
 (** Properties involving Transset and Sum **)
 
 val [prem1,prem2] = goalw QUniv.thy [sum_def]