changeset 173 | 3748d9398c43 |
parent 166 | c59c471126ab |
child 183 | 74ce9774c923 |
--- a/ROOT.ML Wed Nov 23 10:36:03 1994 +0100 +++ b/ROOT.ML Wed Nov 23 10:37:27 1994 +0100 @@ -81,19 +81,6 @@ use "indrule.ML"; use "Inductive.ML"; -(* FIXME -> thy_syntax.ML *) -structure ThySynData = -struct - val user_keywords = ThySynData.user_keywords; - - val user_sections = ThySynData.user_sections @ - [("datatype", datatype_decls), - ("primrec", primrec_decl)]; -end; -structure ThySyn = ThySynFun(ThySynData); -init_thy_reader (); - - use_thy "Finite"; use_thy "List";