src/Pure/NJ.ML

--- a/src/Pure/NJ.ML	Thu May 19 13:13:27 1994 +0200
+++ b/src/Pure/NJ.ML	Thu May 19 13:45:50 1994 +0200
@@ -94,3 +94,9 @@
 
 (*Get pathname of current working directory *)
 fun pwd () = System.Directory.getWD ();
+
+
+(*** ML command execution ***)
+
+fun use_string commands = System.Compile.use_stream (open_string commands);
+