| changeset 17526 | 8d7c587c6b34 |
| parent 17400 | 6ede71a506f5 |
| child 17542 | b588e06b6775 |
--- a/src/Pure/General/pretty.ML Tue Sep 20 18:43:39 2005 +0200 +++ b/src/Pure/General/pretty.ML Tue Sep 20 18:47:42 2005 +0200 @@ -251,7 +251,7 @@ fun output_buffer e = #tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty); val output = Buffer.content o output_buffer; val string_of = Output.raw o output; -val writeln = writeln o string_of; +val writeln = Output.writeln o string_of; fun writelns [] = () | writelns es = writeln (chunks es);