record: tuned output;
authorwenzelm
Fri Oct 24 17:28:20 1997 +0200 (1997-10-24)
changeset 4001b6a3c2665c45
parent 4000 0614fdf0db20
child 4002 6b8abfdf3ec4
record: tuned output;
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Fri Oct 24 17:25:33 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Fri Oct 24 17:28:20 1997 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  val record_decl =
     1.5    name --$$ "=" -- optional (name --$$ "+" >> (parens o cat "Some")) "None" --
     1.6    repeat1 ((name --$$ "::" -- typ) >> mk_pair)
     1.7 -  >> (fn ((x, y), zs) => space_implode " " [x, y, mk_list zs]);
     1.8 +  >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]);
     1.9  
    1.10  
    1.11  (** (co)inductive **)