src/HOL/W0/Maybe.ML

--- a/src/HOL/W0/Maybe.ML	Fri Jan 17 16:17:31 1997 +0100
+++ b/src/HOL/W0/Maybe.ML	Fri Jan 17 16:58:59 1997 +0100
@@ -1,4 +1,9 @@
-open Maybe;
+(* Title:     HOL/W0/Maybe.ML
+   ID:        $Id$
+   Author:    Dieter Nazareth and Tobias Nipkow
+   Copyright  1995 TU Muenchen
+*)
+
 
 (* constructor laws for bind *)
 goalw thy [bind_def] "(Ok s) bind f = (f s)";