# HG changeset patch
# User wenzelm
# Date 870861472 -7200
# Node ID 85898be702b25a79d290b8d819c47b720fd58775
# Parent  d3e24885342886abaf9fd166d32895dac2dbf546
use ThySyn.add_syntax;

diff -r d3e248853428 -r 85898be702b2 src/HOL/thy_syntax.ML
--- 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;
-
diff -r d3e248853428 -r 85898be702b2 src/HOLCF/ax_ops/thy_syntax.ML
--- a/src/HOLCF/ax_ops/thy_syntax.ML	Wed Aug 06 11:57:20 1997 +0200
+++ b/src/HOLCF/ax_ops/thy_syntax.ML	Wed Aug 06 11:57:52 1997 +0200
@@ -5,26 +5,6 @@
 Additional thy file sections for HOLCF: axioms, ops.
 *)
 
-(* use "holcflogics.ML"; 
-   use "thy_axioms.ML";
-   use "thy_ops.ML";      should already have been done in ROOT.ML *)
-
-structure ThySynData : THY_SYN_DATA =
-struct
-
-open HOLCFlogic;
-
-val user_keywords = (*####*)filter_out (fn s => s mem (ThyAxioms.axioms_keywords@
-                    ThyOps.ops_keywords)) (*####*)ThySynData.user_keywords @ 
-                    ThyAxioms.axioms_keywords @ 
-                    ThyOps.ops_keywords;
-
-val user_sections = (*####*)filter_out (fn (s,_) => s mem (map fst (
-                    ThyAxioms.axioms_sections@ ThyOps.ops_sections))) (*####*)
-                      ThySynData.user_sections @
-                    ThyAxioms.axioms_sections @
-                    ThyOps.ops_sections;
-end;
-
-structure ThySyn = ThySynFun(ThySynData);
-set_parser ThySyn.parse;
+ThySyn.add_syntax
+ (ThyAxioms.axioms_keywords @ ThyOps.ops_keywords)
+ (ThyAxioms.axioms_sections @ ThyOps.ops_sections);
diff -r d3e248853428 -r 85898be702b2 src/HOLCF/domain/interface.ML
--- a/src/HOLCF/domain/interface.ML	Wed Aug 06 11:57:20 1997 +0200
+++ b/src/HOLCF/domain/interface.ML	Wed Aug 06 11:57:52 1997 +0200
@@ -6,11 +6,6 @@
 parser for domain section
 *)
 
-
-structure ThySynData: THY_SYN_DATA = (* overwrites old version of ThySynData !!!!!! *)
-
-struct
-
 local 
   open ThyParse;
   open Domain_Library;
@@ -157,14 +152,9 @@
   val gen_by_decl = (optional ($$ "finite" >> K true) false) -- 
 		    (enum1 "," (name'   --$$ "by" -- !!
 			       (enum1 "|" name'))) >> mk_gen_by;
-end; (* local *)
 
-val user_keywords = "lazy"::"by"::"finite"::
-		(**)filter_out (fn s=>s="lazy" orelse s="by" orelse s="finite")(**)
-		    ThySynData.user_keywords;
-val user_sections = ("domain", domain_decl)::("generated", gen_by_decl)::
-		(**)filter_out (fn (s,_)=>s="domain" orelse s="generated")(**)
-		    ThySynData.user_sections;
-end; (* struct *)
+  val _ = ThySyn.add_syntax
+    ["lazy", "by", "finite"]
+    [("domain", domain_decl), ("generated", gen_by_decl)]
 
-structure ThySyn = ThySynFun(ThySynData); (* overwrites old version of ThySyn!!!!!! *)
+end; (* local *)
diff -r d3e248853428 -r 85898be702b2 src/ZF/thy_syntax.ML
--- a/src/ZF/thy_syntax.ML	Wed Aug 06 11:57:20 1997 +0200
+++ b/src/ZF/thy_syntax.ML	Wed Aug 06 11:57:52 1997 +0200
@@ -3,11 +3,11 @@
     Author:     Lawrence C Paulson
     Copyright   1994  University of Cambridge
 
-Additional theory file sections for ZF
+Additional theory file sections for ZF.
 *)
 
-structure ThySynData: THY_SYN_DATA =
-struct
+
+local
 
 (*Inductive definitions theory section.   co is either "" or "Co"*)
 fun inductive_decl co =
@@ -137,18 +137,18 @@
 end;
 
 
-(** Section specifications **)
 
-val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", 
-                     "and", "|", "<=", "domains", "intrs", "monos", 
-                     "con_defs", "type_intrs", "type_elims"];
+(** augment thy syntax **)
+
+in
 
-val user_sections = [("inductive",  inductive_decl ""),
-                     ("coinductive",  inductive_decl "Co"),
-                     ("datatype",  datatype_decl ""),
-                     ("codatatype",  datatype_decl "Co")];
+val _ = ThySyn.add_syntax
+ ["inductive", "coinductive", "datatype", "codatatype", "and", "|",
+  "<=", "domains", "intrs", "monos", "con_defs", "type_intrs",
+  "type_elims"]
+ [("inductive", inductive_decl ""),
+  ("coinductive", inductive_decl "Co"),
+  ("datatype", datatype_decl ""),
+  ("codatatype", datatype_decl "Co")];
+
 end;
-
-
-structure ThySyn = ThySynFun(ThySynData);
-set_parser ThySyn.parse;