author | wenzelm |
Thu, 13 Nov 1997 15:14:14 +0100 | |
changeset 4226 | 38c91213f26b |
parent 4225 | 3d9e551bc5a6 |
child 4227 | a5c947d7c56c |
--- a/src/HOL/thy_syntax.ML Thu Nov 13 12:43:17 1997 +0100 +++ b/src/HOL/thy_syntax.ML Thu Nov 13 15:14:14 1997 +0100 @@ -37,7 +37,7 @@ val record_decl = (type_args -- name >> (mk_pair o apfst mk_list)) --$$ "=" - -- optional (typ --$$ "+" >> cat "Some") "None" + -- optional (typ --$$ "+" >> (parens o cat "Some")) "None" -- repeat1 ((name --$$ "::" -- typ) >> mk_pair) >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]);