diff -r 33d50643dccc -r 2f3a2d9054d1 ROOT.ML
--- a/ROOT.ML	Fri Jun 17 18:34:12 1994 +0200
+++ b/ROOT.ML	Mon Jun 20 12:05:03 1994 +0200
@@ -11,7 +11,7 @@
 writeln banner;
 
 (* Add user section "datatype" *)
-use     "Datatype";
+use     "Datatype.ML";
 structure ThySyn = ThySynFun(val user_keywords = ["|", "datatype"] and
   user_sections = [("datatype",  datatype_decls)]);
 init_thy_reader ();