src/Pure/ML-Systems/smlnj.ML
changeset 26885 cfd5eb167706
parent 26884 67c54c53da28
child 28151 61f9c918b410
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed May 14 11:05:45 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed May 14 11:09:07 2008 +0200
     1.3 @@ -129,14 +129,14 @@
     1.4      if verbose then print (output ()) else ()
     1.5    end;
     1.6  
     1.7 -fun use_file tune _ output verbose name =
     1.8 +fun use_file tune str_of_pos output verbose name =
     1.9    let
    1.10      val instream = TextIO.openIn name;
    1.11      val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    1.12 -  in use_text tune (1, name) output verbose txt end;
    1.13 +  in use_text tune str_of_pos (1, name) output verbose txt end;
    1.14  
    1.15  fun forget_structure name =
    1.16 -  use_text (fn x => x) (1, "ML") (TextIO.print, fn s => raise Fail s) false
    1.17 +  use_text (fn x => x) (fn _ => "") (1, "ML") (TextIO.print, fn s => raise Fail s) false
    1.18      ("structure " ^ name ^ " = struct end");
    1.19  
    1.20