--- a/src/Pure/ML-Systems/polyml_old_compiler5.ML Wed Sep 17 21:27:22 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML Wed Sep 17 21:27:24 2008 +0200
@@ -4,7 +4,7 @@
Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1).
*)
-fun use_text (tune: string -> string) _ (line, name) (print, err) verbose txt =
+fun use_text (tune: string -> string) _ _ (line, name) (print, err) verbose txt =
let
val in_buffer = ref (explode (tune txt));
val out_buffer = ref ([]: string list);
@@ -26,9 +26,8 @@
if verbose then print (output ()) else ()
end;
-fun use_file tune str_of_pos output verbose name =
+fun use_file tune str_of_pos name_space output verbose name =
let
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 (1, name) output verbose txt end;
-
+ in use_text tune str_of_pos name_space (1, name) output verbose txt end;