ROOT.ML
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";