src/Pure/General/buffer.ML

--- a/src/Pure/General/buffer.ML	Wed Aug 27 20:36:25 2008 +0200
+++ b/src/Pure/General/buffer.ML	Wed Aug 27 20:36:26 2008 +0200
@@ -14,7 +14,6 @@
   val markup: Markup.T -> (T -> T) -> T -> T
   val content: T -> string
   val output: T -> TextIO.outstream -> unit
-  val write: Path.T -> T -> unit
 end;
 
 structure Buffer: BUFFER =
@@ -62,6 +61,4 @@
       | rev_output (Substring (s, buf)) = (TextIO.outputSubstr (stream, s); rev_output buf);
   in rev_output (rev_buffer buffer empty) end;
 
-fun write path buf = File.open_output (output buf) path;
-
 end;