src/Pure/ML-Systems/mosml.ML
changeset 26884 67c54c53da28
parent 26504 6e87c0a60104
child 27003 aae9b369b338
--- 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;