diff -r e0d0e5b4994f -r 5f99df1e26c4 ROOT.ML
--- a/ROOT.ML	Wed Aug 03 11:00:40 1994 +0200
+++ b/ROOT.ML	Sat Aug 13 16:33:53 1994 +0200
@@ -12,8 +12,10 @@
 
 (* 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;