moved remaining thy syntax stuff to thy_syntax.ML;
authorwenzelm
Wed, 23 Nov 1994 10:37:27 +0100
changeset 173 3748d9398c43
parent 172 8aa51768ade4
child 174 c843e5a4e0a4
moved remaining thy syntax stuff to thy_syntax.ML;
ROOT.ML
--- 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";