1.1 --- a/src/Pure/ML-Systems/polyml_old_compiler4.ML	Wed May 14 11:05:11 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Wed May 14 11:05:45 2008 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  Runtime compilation -- for old PolyML.compiler (version 4.x).
     1.5  *)
     1.6  
     1.7 -fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt =
     1.8 +fun use_text (tune: string -> string) _ (line: int, name) (print, err) verbose txt =
     1.9    let
    1.10      val in_buffer = ref (explode (tune txt));
    1.11      val out_buffer = ref ([]: string list);
    1.12 @@ -26,7 +26,7 @@
    1.13      if verbose then print (output ()) else ()
    1.14    end;
    1.15  
    1.16 -fun use_file tune output verbose name =
    1.17 +fun use_file tune _ output verbose name =
    1.18    let
    1.19      val instream = TextIO.openIn name;
    1.20      val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);