ROOT.ML
changeset 86 2f3a2d9054d1
parent 80 d3d727449d7b
child 101 5f99df1e26c4
--- 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 ();