| changeset 15570 | 8d8c70b41bab |
| parent 14995 | 318e58f49e8d |
| child 16714 | d9e3ef66b38c |
--- a/src/Pure/General/pretty.ML Thu Mar 03 09:22:35 2005 +0100 +++ b/src/Pure/General/pretty.ML Thu Mar 03 12:43:01 2005 +0100 @@ -204,7 +204,7 @@ blk (1, [str "\"", prt, str "\""]); fun commas prts = - flat (separate [str ",", brk 1] (map (fn x => [x]) prts)); + List.concat (separate [str ",", brk 1] (map (fn x => [x]) prts)); fun breaks prts = separate (brk 1) prts; fun fbreaks prts = separate fbrk prts;