tuned write: use File.write_list;

--- a/src/Pure/General/buffer.ML	Wed Jul 06 10:41:45 2005 +0200
+++ b/src/Pure/General/buffer.ML	Wed Jul 06 10:41:46 2005 +0200
@@ -22,6 +22,6 @@
 val empty = Buffer [];
 fun add x (Buffer xs) = Buffer (x :: xs);
 fun content (Buffer xs) = implode (rev xs);
-fun write path buffer = File.write path (content buffer);
+fun write path (Buffer xs) = File.write_list path (rev xs);
 
 end;