src/Pure/ML-Systems/polyml.ML

     val instream = TextIO.openIn name;
     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
   in use_text tune str_of_pos name_space (1, name) output verbose txt end;
 
 end;
+
+use "ML-Systems/polyml_pp.ML";
+