src/Pure/ML-Systems/mosml.ML
changeset 26884 67c54c53da28
parent 26504 6e87c0a60104
child 27003 aae9b369b338
     1.1 --- a/src/Pure/ML-Systems/mosml.ML	Wed May 14 11:05:11 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/mosml.ML	Wed May 14 11:05:45 2008 +0200
     1.3 @@ -152,7 +152,7 @@
     1.4  (* ML command execution *)
     1.5  
     1.6  (*Can one redirect 'use' directly to an instream?*)
     1.7 -fun use_text (tune: string -> string) _ _ _ txt =
     1.8 +fun use_text (tune: string -> string) _ _ _ _ txt =
     1.9    let
    1.10      val tmp_name = FileSys.tmpName ();
    1.11      val tmp_file = TextIO.openOut tmp_name;
    1.12 @@ -163,7 +163,7 @@
    1.13      FileSys.remove tmp_name
    1.14    end;
    1.15  
    1.16 -fun use_file _ _ _ name = use name;
    1.17 +fun use_file _ _ _ _ name = use name;
    1.18  
    1.19  
    1.20