diff -r 6eb89a693e05 -r 2edd7a39d92a src/Pure/NJ.ML
--- a/src/Pure/NJ.ML	Sun Oct 22 15:16:57 1995 +0100
+++ b/src/Pure/NJ.ML	Tue Oct 24 13:40:06 1995 +0100
@@ -102,3 +102,19 @@
 fun use_string commands = 
   System.Compile.use_stream (open_string (implode commands));
 
+
+(*** System command execution ***)
+
+(*Execute an Unix command which doesn't take any input from stdin and
+  sends its output to stdout.
+  This could be done more easily by IO.execute, but that function
+  seems to be buggy in SML/NJ 0.93.*)
+fun execute command =
+  let val tmp_name = "isa_converted.tmp"
+      val is = (System.system (command ^ " > " ^ tmp_name);
+                open_in tmp_name);
+      val result = input (is, 999999);
+  in close_in is;
+     delete_file tmp_name;
+     result
+  end;