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));