diff -r 4dec4460244f -r 6e87c0a60104 src/Pure/ML-Systems/polyml_old_compiler4.ML
--- a/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 31 23:08:54 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 31 23:08:55 2008 +0200
@@ -29,6 +29,6 @@
 fun use_file tune output verbose name =
   let
     val instream = TextIO.openIn name;
-    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
+    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
   in use_text tune (1, name) output verbose txt end;