# HG changeset patch
# User wenzelm
# Date 1656062414 -7200
# Node ID 1b50bcd108b75485a727e5062e4d691f4cfbce8e
# Parent  03ae0ba2aa9e238e7f44286be3467356f6c019b4
unused;

diff -r 03ae0ba2aa9e -r 1b50bcd108b7 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Fri Jun 24 10:55:23 2022 +0200
+++ b/src/Pure/General/file.ML	Fri Jun 24 11:20:14 2022 +0200
@@ -38,7 +38,6 @@
   val outputs: BinIO.outstream -> string list -> unit
   val write_list: Path.T -> string list -> unit
   val append_list: Path.T -> string list -> unit
-  val write_buffer: Path.T -> Buffer.T -> unit
   val eq: Path.T * Path.T -> bool
 end;
 
@@ -170,9 +169,6 @@
 fun write path txt = write_list path [txt];
 fun append path txt = append_list path [txt];
 
-fun write_buffer path buf =
-  open_output (fn file => List.app (output file) (Buffer.contents buf)) path;
-
 
 (* eq *)