# HG changeset patch
# User wenzelm
# Date 785583447 -3600
# Node ID 3748d9398c43b67a779af79ea7730ada6bee73b0
# Parent  8aa51768ade4d1834ce2cdc1651c01ac1b0fea8f
moved remaining thy syntax stuff to thy_syntax.ML;

diff -r 8aa51768ade4 -r 3748d9398c43 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";