ROOT.ML

 val banner = "Higher-Order Logic";
 writeln banner;
 
 (* Add user section "datatype" *)
 use     "Datatype.ML";
-structure ThySyn = ThySynFun(val user_keywords = ["|", "datatype"] and
-  user_sections = [("datatype",  datatype_decls)]);
+structure ThySyn =
+  ThySynFun(val user_keywords = ["|", "datatype", "primrec"]
+            and user_sections = [("datatype",  datatype_decls),
+                                 ("primrec", primrec_decl)]);
 init_thy_reader ();
 
 print_depth 1;  
 eta_contract := true;
 use_thy "HOL";