diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/Datatype.thy
--- a/src/ZF/Datatype.thy	Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/Datatype.thy	Fri Aug 12 12:51:34 1994 +0200
@@ -1,4 +1,5 @@
 (*Dummy theory to document dependencies *)
 
-Datatype = "constructor" + "inductive" + "coinductive" + Univ + QUniv
-               (*this must be capital to avoid conflicts with ML's "datatype" *)
\ No newline at end of file
+Datatype = "constructor" + "inductive" + Univ + QUniv
+
+(*Datatype must be capital to avoid conflicts with ML's "datatype" *)
\ No newline at end of file