src/Pure/ML-Systems/smlnj.ML
changeset 26504 6e87c0a60104
parent 26474 94735cff132c
child 26884 67c54c53da28
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Mar 31 23:08:54 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Mar 31 23:08:55 2008 +0200
     1.3 @@ -132,7 +132,7 @@
     1.4  fun use_file tune output verbose name =
     1.5    let
     1.6      val instream = TextIO.openIn name;
     1.7 -    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
     1.8 +    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
     1.9    in use_text tune (1, name) output verbose txt end;
    1.10  
    1.11  fun forget_structure name =