src/Pure/General/file.ML
changeset 75613 1b50bcd108b7
parent 75604 39df30349778
child 75615 4494cd69f97f
--- 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 *)