--- 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 *)