# HG changeset patch
# User wenzelm
# Date 877603756 -7200
# Node ID 21ef91734970fdc0d6165de669329ff3a4009afc
# Parent  dac05c9341f4b4c488c9accd3f4fa401ece81e66
added record section;

diff -r dac05c9341f4 -r 21ef91734970 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Thu Oct 23 12:48:48 1997 +0200
+++ b/src/HOL/thy_syntax.ML	Thu Oct 23 12:49:16 1997 +0200
@@ -36,6 +36,14 @@
 
 
 
+(** record **)
+
+val record_decl =
+  name --$$ "=" -- optional (name --$$ "+" >> (parens o cat "Some")) "None" --
+  repeat1 ((name --$$ "::" -- typ) >> mk_pair)
+  >> (fn ((x, y), zs) => space_implode " " [x, y, mk_list zs]);
+
+
 (** (co)inductive **)
 
 (*co is either "" or "Co"*)
@@ -122,7 +130,7 @@
     ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
     \val thy = ("^tname^"_add_primrec "^tname^"_size_eqns thy)"
     ,
-    "val _ = deny (" ^ quote tname ^ " mem  map ! (stamps_of_thy thy))\n\
+    "val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\
     \   (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
     \structure " ^ tname ^ " =\n\
     \struct\n\
@@ -269,6 +277,7 @@
 val _ = ThySyn.add_syntax
  ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
  [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
+  (section "record" "|> Record.add_record" record_decl),
   ("inductive", inductive_decl ""),
   ("coinductive", inductive_decl "Co"),
   ("datatype", datatype_decl),