src/HOL/thy_syntax.ML
changeset 3980 21ef91734970
parent 3945 ae9c61d69888
child 4001 b6a3c2665c45
     1.1 --- a/src/HOL/thy_syntax.ML	Thu Oct 23 12:48:48 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Oct 23 12:49:16 1997 +0200
     1.3 @@ -36,6 +36,14 @@
     1.4  
     1.5  
     1.6  
     1.7 +(** record **)
     1.8 +
     1.9 +val record_decl =
    1.10 +  name --$$ "=" -- optional (name --$$ "+" >> (parens o cat "Some")) "None" --
    1.11 +  repeat1 ((name --$$ "::" -- typ) >> mk_pair)
    1.12 +  >> (fn ((x, y), zs) => space_implode " " [x, y, mk_list zs]);
    1.13 +
    1.14 +
    1.15  (** (co)inductive **)
    1.16  
    1.17  (*co is either "" or "Co"*)
    1.18 @@ -122,7 +130,7 @@
    1.19      ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
    1.20      \val thy = ("^tname^"_add_primrec "^tname^"_size_eqns thy)"
    1.21      ,
    1.22 -    "val _ = deny (" ^ quote tname ^ " mem  map ! (stamps_of_thy thy))\n\
    1.23 +    "val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\
    1.24      \   (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
    1.25      \structure " ^ tname ^ " =\n\
    1.26      \struct\n\
    1.27 @@ -269,6 +277,7 @@
    1.28  val _ = ThySyn.add_syntax
    1.29   ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
    1.30   [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
    1.31 +  (section "record" "|> Record.add_record" record_decl),
    1.32    ("inductive", inductive_decl ""),
    1.33    ("coinductive", inductive_decl "Co"),
    1.34    ("datatype", datatype_decl),