--- 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;
-
--- 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);
--- 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 *)
--- 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;