diff -r fe7b7e3c3ddc -r 092a6435afad src/Pure/ML-Systems/mlworks.ML
--- a/src/Pure/ML-Systems/mlworks.ML	Wed Oct 13 19:42:12 1999 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML	Wed Oct 13 19:42:46 1999 +0200
@@ -78,7 +78,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;
@@ -121,6 +121,10 @@
     result
   end;
 
+(*plain version; with return code*)
+fun system cmd =
+  if OS.Process.system cmd = OS.Process.success then 0 else 1;
+
 
 (* file handling *)