diff -r d9527f97246e -r 89669c58e506 ROOT.ML
--- a/ROOT.ML	Thu Aug 25 10:47:33 1994 +0200
+++ b/ROOT.ML	Thu Aug 25 11:01:45 1994 +0200
@@ -10,13 +10,7 @@
 val banner = "Higher-Order Logic";
 writeln banner;
 
-(* Add user section "datatype" *)
-use     "Datatype.ML";
-structure ThySyn =
-  ThySynFun(val user_keywords = ["|", "datatype", "primrec"]
-            and user_sections = [("datatype",  datatype_decls),
-                                 ("primrec", primrec_decl)]);
-init_thy_reader ();
+init_thy_reader();
 
 print_depth 1;  
 eta_contract := true;
@@ -81,6 +75,29 @@
 use_thy "equalities";
 use_thy "Prod";
 use_thy "Sum";
+use_thy "Gfp";
+use_thy "Nat";
+
+(* Add user sections *)
+use     "Datatype.ML";
+use "../Pure/section_utils.ML";
+use "ind_syntax.ML";
+use "add_ind_def.ML";
+use "intr_elim.ML";
+use "indrule.ML";
+use "Inductive.ML";
+
+structure ThySyn = ThySynFun
+ (val user_keywords = ["|", "datatype", "primrec",
+		       "inductive", "coinductive", "intrs", 
+		       "monos", "con_defs"]
+  and user_sections = [("inductive",  inductive_decl ""),
+		       ("coinductive",  inductive_decl "Co"),
+		       ("datatype",  datatype_decls),
+		       ("primrec", primrec_decl)]);
+init_thy_reader ();
+
+use_thy "Finite";
 use_thy "LList";
 
 use "../Pure/install_pp.ML";