src/Pure/ML-Systems/smlnj-0.93.ML
changeset 5038 301c37df931d
parent 4977 6cec2c0ffdbf
child 5090 75ac9b451ae0
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Mon Jun 15 11:05:25 1998 +0200
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Mon Jun 15 11:06:00 1998 +0200
@@ -81,8 +81,7 @@
 
 (* ML command execution *)
 
-fun use_strings commands =
-  System.Compile.use_stream (open_string (implode commands));
+val use_text = System.Compile.use_stream o open_string;