--- a/src/Pure/ML-Systems/smlnj-1.09.ML Mon Dec 16 10:04:12 1996 +0100
+++ b/src/Pure/ML-Systems/smlnj-1.09.ML Mon Dec 16 10:04:45 1996 +0100
@@ -107,3 +107,8 @@
OS.FileSys.remove tmp_name;
result
end;
+
+
+(* symbol input *)
+
+val needs_filtered_use = false;