use_text/file: ignore str_of_pos argument;

--- a/src/Pure/ML-Systems/alice.ML	Wed May 14 11:05:11 2008 +0200
+++ b/src/Pure/ML-Systems/alice.ML	Wed May 14 11:05:45 2008 +0200
@@ -119,8 +119,8 @@
 
 (* ML command execution *)
 
-fun use_text _ _ _ _ txt = (Compiler.eval txt; ());
-fun use_file _ _ _ name = use name;
+fun use_text _ _ _ _ _ txt = (Compiler.eval txt; ());
+fun use_file _ _ _ _ name = use name;
 
 
 

--- a/src/Pure/ML-Systems/mosml.ML	Wed May 14 11:05:11 2008 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Wed May 14 11:05:45 2008 +0200
@@ -152,7 +152,7 @@
 (* ML command execution *)
 
 (*Can one redirect 'use' directly to an instream?*)
-fun use_text (tune: string -> string) _ _ _ txt =
+fun use_text (tune: string -> string) _ _ _ _ txt =
   let
     val tmp_name = FileSys.tmpName ();
     val tmp_file = TextIO.openOut tmp_name;
@@ -163,7 +163,7 @@
     FileSys.remove tmp_name
   end;
 
-fun use_file _ _ _ name = use name;
+fun use_file _ _ _ _ name = use name;
 
 
 

--- a/src/Pure/ML-Systems/polyml_old_compiler4.ML	Wed May 14 11:05:11 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Wed May 14 11:05:45 2008 +0200
@@ -4,7 +4,7 @@
 Runtime compilation -- for old PolyML.compiler (version 4.x).
 *)
 
-fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt =
+fun use_text (tune: string -> string) _ (line: int, name) (print, err) verbose txt =
   let
     val in_buffer = ref (explode (tune txt));
     val out_buffer = ref ([]: string list);
@@ -26,7 +26,7 @@
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune output verbose name =
+fun use_file tune _ output verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);

--- a/src/Pure/ML-Systems/polyml_old_compiler5.ML	Wed May 14 11:05:11 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML	Wed May 14 11:05:45 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,7 +26,7 @@
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune output verbose name =
+fun use_file tune _ output verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);

--- a/src/Pure/ML-Systems/poplogml.ML	Wed May 14 11:05:11 2008 +0200
+++ b/src/Pure/ML-Systems/poplogml.ML	Wed May 14 11:05:45 2008 +0200
@@ -374,5 +374,5 @@
 
 end;
 
-fun use_text _ _ _ txt = use_string txt;
-fun use_file _ _ name = use name;
+fun use_text _ _ _ _ txt = use_string txt;
+fun use_file _ _ _ name = use name;

--- a/src/Pure/ML-Systems/smlnj.ML	Wed May 14 11:05:11 2008 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed May 14 11:05:45 2008 +0200
@@ -111,7 +111,7 @@
 
 (* ML command execution *)
 
-fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt =
+fun use_text (tune: string -> string) _ (line: int, name) (print, err) verbose txt =
   let
     val ref out_orig = Control.Print.out;
 
@@ -129,7 +129,7 @@
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune output verbose name =
+fun use_file tune _ output verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);