Datatype -> Datatype.ML
authornipkow
Mon, 20 Jun 1994 12:05:03 +0200
changeset 86 2f3a2d9054d1
parent 85 33d50643dccc
child 87 b0ea0e55dfe8
Datatype -> Datatype.ML
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 ();