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