# HG changeset patch
# User wenzelm
# Date 939291561 -7200
# Node ID 659648e14c3ef050c38377c28436a717953f8319
# Parent  444ac56ead9142895e7b1f0ea510772e491e6f35
removed write_nonempty;

diff -r 444ac56ead91 -r 659648e14c3e src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Thu Oct 07 11:39:47 1999 +0200
+++ b/src/Pure/General/buffer.ML	Thu Oct 07 12:19:21 1999 +0200
@@ -12,7 +12,6 @@
   val add: string -> T -> T
   val content: T -> string
   val write: Path.T -> T -> unit
-  val write_nonempty: Path.T -> T -> unit
 end;
 
 structure Buffer: BUFFER =
@@ -21,13 +20,8 @@
 datatype T = Buffer of string list;
 
 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_nonempty _ (Buffer []) = ()
-  | write_nonempty path buffer = write path buffer;
-
 end;