diff -r 1df7ad3a6082 -r 7272b45099c7 src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Tue Aug 16 13:42:32 2005 +0200
+++ b/src/Pure/General/buffer.ML	Tue Aug 16 13:42:33 2005 +0200
@@ -20,8 +20,12 @@
 datatype T = Buffer of string list;
 
 val empty = Buffer [];
-fun add x (Buffer xs) = Buffer (x :: xs);
+
+fun add "" buf = buf
+  | add x (Buffer xs) = Buffer (x :: xs);
+
 fun content (Buffer xs) = implode (rev xs);
+
 fun write path (Buffer xs) = File.write_list path (rev xs);
 
 end;