| changeset 23226 | 441f8a0bd766 |
| parent 21630 | d1ca26a2b918 |
| child 23785 | ea7c2ee8a47a |
--- a/src/Pure/General/buffer.ML Sun Jun 03 23:16:53 2007 +0200 +++ b/src/Pure/General/buffer.ML Sun Jun 03 23:16:54 2007 +0200 @@ -29,6 +29,6 @@ fun write path (Buffer xs) = File.write_list path (rev xs); -fun output f (Buffer xs) = Library.seq f (rev xs); +fun output f (Buffer xs) = List.app f (rev xs); end;