src/Pure/ML-Systems/smlnj.ML
changeset 5038 301c37df931d
parent 4977 6cec2c0ffdbf
child 5090 75ac9b451ae0
--- a/src/Pure/ML-Systems/smlnj.ML	Mon Jun 15 11:05:25 1998 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Jun 15 11:06:00 1998 +0200
@@ -82,7 +82,7 @@
 
 (* ML command execution *)
 
-val use_strings = Compiler.Interact.useStream o TextIO.openString o implode;
+val use_text = Compiler.Interact.useStream o TextIO.openString;