# HG changeset patch
# User wenzelm
# Date 879421397 -3600
# Node ID 3d9e551bc5a6576b1c867cb83e5cc0cf0d2c7b46
# Parent  79e205c3a82c7c2532a640621a25fd4ba7297635
improved record syntax;

diff -r 79e205c3a82c -r 3d9e551bc5a6 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Thu Nov 13 10:31:42 1997 +0100
+++ b/src/HOL/thy_syntax.ML	Thu Nov 13 12:43:17 1997 +0100
@@ -36,8 +36,9 @@
 (** record **)
 
 val record_decl =
-  name --$$ "=" -- optional (name --$$ "+" >> (parens o cat "Some")) "None" --
-  repeat1 ((name --$$ "::" -- typ) >> mk_pair)
+  (type_args -- name >> (mk_pair o apfst mk_list)) --$$ "="
+    -- optional (typ --$$ "+" >> cat "Some") "None"
+    -- repeat1 ((name --$$ "::" -- typ) >> mk_pair)
   >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]);