--- a/src/Pure/NJ1xx.ML Mon Dec 02 10:23:28 1996 +0100
+++ b/src/Pure/NJ1xx.ML Mon Dec 02 10:25:53 1996 +0100
@@ -87,13 +87,15 @@
(*** ML command execution ***)
+
+(*For version 109.21 and later:
+val use_string = Compiler.Interact.useStream o TextIO.openString o implode;
+*)
+
+(*For versions prior to 109.21:*)
fun use_string commands =
Compiler.Interact.use_stream (open_string (implode commands));
-(*For later versions of Standard ML of New Jersey use...
-val use_string = Compiler.Interact.useStream o TextIO.openString o implode;
-*)
-
(*** System command execution ***)
(*Execute an Unix command which doesn't take any input from stdin and