changeset 101 | 5f99df1e26c4 |
parent 86 | 2f3a2d9054d1 |
child 119 | 93dc86ccee28 |
--- 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;