src/Pure/POLY.ML

--- a/src/Pure/POLY.ML	Sun Oct 22 15:16:57 1995 +0100
+++ b/src/Pure/POLY.ML	Tue Oct 24 13:40:06 1995 +0100
@@ -103,3 +103,16 @@
   in seq exec end;
 
 end;
+
+
+(*** System command execution ***)
+
+(*Execute an Unix command which doesn't take any input from stdin and
+  sends its output to stdout.*)
+fun execute command =
+  let val (is, os) =  ExtendedIO.execute command;
+      val result = input (is, 999999);
+  in close_out os;
+     close_in is;
+     result
+  end;