src/Pure/ML-Systems/mlworks.ML
changeset 5090 75ac9b451ae0
parent 5038 301c37df931d
child 5660 f2c5354cd32f
--- a/src/Pure/ML-Systems/mlworks.ML	Fri Jun 26 15:16:14 1998 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML	Mon Jun 29 10:32:06 1998 +0200
@@ -66,7 +66,7 @@
 (* ML command execution *)
 
 (*Can one redirect 'use' directly to an instream?*)
-fun use_text txt =
+fun use_text _ txt =
   let
     val tmp_name = OS.FileSys.tmpName ();
     val tmp_file = TextIO.openOut tmp_name;