unused;
authorwenzelm
Fri, 24 Jun 2022 11:20:14 +0200
changeset 75613 1b50bcd108b7
parent 75612 03ae0ba2aa9e
child 75614 01b3da984e55
unused;
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 *)