changeset 4001 | b6a3c2665c45 |
parent 3980 | 21ef91734970 |
child 4032 | 4b1c69d8b767 |
--- a/src/HOL/thy_syntax.ML Fri Oct 24 17:25:33 1997 +0200 +++ b/src/HOL/thy_syntax.ML Fri Oct 24 17:28:20 1997 +0200 @@ -41,7 +41,7 @@ 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]); + >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]); (** (co)inductive **)