diff -r a3b8d0a0250d -r cfbd814a11f2 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Aug 08 00:11:11 1997 +0200
+++ b/src/Pure/library.ML	Fri Aug 08 11:22:59 1997 +0200
@@ -783,9 +783,13 @@
   end;
 
 fun write_file name txt =
-  let
-    val outstream = TextIO.openOut name;
-  in
+  let val outstream = TextIO.openOut name in
+    TextIO.output (outstream, txt);
+    TextIO.closeOut outstream
+  end;
+
+fun append_file name txt =
+  let val outstream = TextIO.openAppend name in
     TextIO.output (outstream, txt);
     TextIO.closeOut outstream
   end;