diff -r 712dceb1ecc7 -r 18c9c28d0f7e src/Pure/NJ.ML
--- a/src/Pure/NJ.ML	Thu May 26 12:55:52 1994 +0200
+++ b/src/Pure/NJ.ML	Thu May 26 13:37:51 1994 +0200
@@ -98,5 +98,6 @@
 
 (*** ML command execution ***)
 
-fun use_string commands = System.Compile.use_stream (open_string commands);
+fun use_string commands = 
+  System.Compile.use_stream (open_string (implode commands));