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;