src/Pure/General/file.ML
changeset 75604 39df30349778
parent 75595 ecbd0b38256b
child 75613 1b50bcd108b7
--- a/src/Pure/General/file.ML	Thu Jun 23 21:25:56 2022 +0200
+++ b/src/Pure/General/file.ML	Thu Jun 23 21:50:32 2022 +0200
@@ -34,7 +34,6 @@
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
-  val generate: Path.T -> string -> unit
   val output: BinIO.outstream -> string -> unit
   val outputs: BinIO.outstream -> string list -> unit
   val write_list: Path.T -> string list -> unit
@@ -170,7 +169,6 @@
 
 fun write path txt = write_list path [txt];
 fun append path txt = append_list path [txt];
-fun generate path txt = if try read path = SOME txt then () else write path txt;
 
 fun write_buffer path buf =
   open_output (fn file => List.app (output file) (Buffer.contents buf)) path;