src/Pure/ML-Systems/smlnj-0.93.ML
changeset 5090 75ac9b451ae0
parent 5038 301c37df931d
child 5816 6f3cb53502fa
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Fri Jun 26 15:16:14 1998 +0200
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Mon Jun 29 10:32:06 1998 +0200
@@ -81,7 +81,7 @@
 
 (* ML command execution *)
 
-val use_text = System.Compile.use_stream o open_string;
+fun use_text _ = System.Compile.use_stream o open_string;