src/Pure/library.ML
changeset 3645 cfbd814a11f2
parent 3624 36e19fce289e
child 3699 7c30ab9e25d1
     1.1 --- a/src/Pure/library.ML	Fri Aug 08 00:11:11 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Fri Aug 08 11:22:59 1997 +0200
     1.3 @@ -783,9 +783,13 @@
     1.4    end;
     1.5  
     1.6  fun write_file name txt =
     1.7 -  let
     1.8 -    val outstream = TextIO.openOut name;
     1.9 -  in
    1.10 +  let val outstream = TextIO.openOut name in
    1.11 +    TextIO.output (outstream, txt);
    1.12 +    TextIO.closeOut outstream
    1.13 +  end;
    1.14 +
    1.15 +fun append_file name txt =
    1.16 +  let val outstream = TextIO.openAppend name in
    1.17      TextIO.output (outstream, txt);
    1.18      TextIO.closeOut outstream
    1.19    end;