--- a/ROOT.ML Wed Jun 15 19:28:35 1994 +0200
+++ b/ROOT.ML Fri Jun 17 14:15:38 1994 +0200
@@ -10,7 +10,11 @@
val banner = "Higher-Order Logic";
writeln banner;
-init_thy_reader();
+(* Add user section "datatype" *)
+use "Datatype";
+structure ThySyn = ThySynFun(val user_keywords = ["|", "datatype"] and
+ user_sections = [("datatype", datatype_decls)]);
+init_thy_reader ();
print_depth 1;
eta_contract := true;
@@ -79,7 +83,6 @@
use_thy "Sum";
use "mono.ML";
use_thy "LList";
-use_thy "Datatype";
use "../Pure/install_pp.ML";
print_depth 8;