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