src/HOL/thy_syntax.ML
changeset 3622 85898be702b2
parent 3617 b689656214ea
child 3665 3b44fac767f6
     1.1 --- a/src/HOL/thy_syntax.ML	Wed Aug 06 11:57:20 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Wed Aug 06 11:57:52 1997 +0200
     1.3 @@ -11,8 +11,8 @@
     1.4  (*the kind of distinctiveness axioms depends on number of constructors*)
     1.5  val dtK = 7;  (* FIXME rename?, move? *)
     1.6  
     1.7 -structure ThySynData: THY_SYN_DATA =
     1.8 -struct
     1.9 +
    1.10 +local
    1.11  
    1.12  open ThyParse;
    1.13  
    1.14 @@ -259,13 +259,12 @@
    1.15  
    1.16  
    1.17  
    1.18 -
    1.19 -
    1.20 -(** sections **)
    1.21 +(** augment thy syntax **)
    1.22  
    1.23 -val user_keywords = ["intrs", "monos", "con_defs", "congs", "simpset", "|"];
    1.24 +in
    1.25  
    1.26 -val user_sections =
    1.27 +val _ = ThySyn.add_syntax
    1.28 + ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
    1.29   [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
    1.30    ("inductive", inductive_decl ""),
    1.31    ("coinductive", inductive_decl "Co"),
    1.32 @@ -273,10 +272,4 @@
    1.33    ("primrec", primrec_decl),
    1.34    ("recdef", rec_decl)];
    1.35  
    1.36 -
    1.37  end;
    1.38 -
    1.39 -
    1.40 -structure ThySyn = ThySynFun(ThySynData);
    1.41 -set_parser ThySyn.parse;
    1.42 -