diff -r efd3e5a2d493 -r d3d727449d7b ROOT.ML
--- 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;