# HG changeset patch
# User wenzelm
# Date 1210756147 -7200
# Node ID cfd5eb1677064205c1d196a24819a832e59edb03
# Parent  67c54c53da283a7e74d4b7b8cce3377bc015d871
use_file: pass str_of_pos;

diff -r 67c54c53da28 -r cfd5eb167706 src/Pure/ML-Systems/polyml_old_compiler4.ML
--- a/src/Pure/ML-Systems/polyml_old_compiler4.ML	Wed May 14 11:05:45 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Wed May 14 11:09:07 2008 +0200
@@ -26,9 +26,9 @@
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune _ output verbose name =
+fun use_file tune str_of_pos 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 (1, name) output verbose txt end;
+  in use_text tune str_of_pos (1, name) output verbose txt end;
 
diff -r 67c54c53da28 -r cfd5eb167706 src/Pure/ML-Systems/polyml_old_compiler5.ML
--- a/src/Pure/ML-Systems/polyml_old_compiler5.ML	Wed May 14 11:05:45 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML	Wed May 14 11:09:07 2008 +0200
@@ -26,9 +26,9 @@
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune _ output verbose name =
+fun use_file tune str_of_pos 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 (1, name) output verbose txt end;
+  in use_text tune str_of_pos (1, name) output verbose txt end;
 
diff -r 67c54c53da28 -r cfd5eb167706 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Wed May 14 11:05:45 2008 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed May 14 11:09:07 2008 +0200
@@ -129,14 +129,14 @@
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune _ output verbose name =
+fun use_file tune str_of_pos 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 (1, name) output verbose txt end;
+  in use_text tune str_of_pos (1, name) output verbose txt end;
 
 fun forget_structure name =
-  use_text (fn x => x) (1, "ML") (TextIO.print, fn s => raise Fail s) false
+  use_text (fn x => x) (fn _ => "") (1, "ML") (TextIO.print, fn s => raise Fail s) false
     ("structure " ^ name ^ " = struct end");