--- a/src/HOL/thy_syntax.ML Wed Aug 06 11:57:20 1997 +0200
+++ b/src/HOL/thy_syntax.ML Wed Aug 06 11:57:52 1997 +0200
@@ -11,8 +11,8 @@
(*the kind of distinctiveness axioms depends on number of constructors*)
val dtK = 7; (* FIXME rename?, move? *)
-structure ThySynData: THY_SYN_DATA =
-struct
+
+local
open ThyParse;
@@ -259,13 +259,12 @@
-
-
-(** sections **)
+(** augment thy syntax **)
-val user_keywords = ["intrs", "monos", "con_defs", "congs", "simpset", "|"];
+in
-val user_sections =
+val _ = ThySyn.add_syntax
+ ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
[axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
("inductive", inductive_decl ""),
("coinductive", inductive_decl "Co"),
@@ -273,10 +272,4 @@
("primrec", primrec_decl),
("recdef", rec_decl)];
-
end;
-
-
-structure ThySyn = ThySynFun(ThySynData);
-set_parser ThySyn.parse;
-