added needs_filtered_use;

--- a/src/Pure/ML-Systems/polyml.ML	Mon Dec 16 10:04:12 1996 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Dec 16 10:04:45 1996 +0100
@@ -117,3 +117,11 @@
      close_in is;
      result
   end;
+
+
+(* symbol input *)
+
+val needs_filtered_use =
+  (case explode ml_system of
+    "p" :: "o" :: "l" :: "y" :: "m" :: "l" :: "-" :: "3" :: _ => true
+  | _ => false);

--- 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;

--- a/src/Pure/NJ093.ML	Mon Dec 16 10:04:12 1996 +0100
+++ b/src/Pure/NJ093.ML	Mon Dec 16 10:04:45 1996 +0100
@@ -120,3 +120,6 @@
 
 (*For use in Makefiles -- saves space*)
 fun xML filename banner = (exportML filename;  print(banner^"\n"));
+
+
+val needs_filtered_use = false;

--- a/src/Pure/NJ1xx.ML	Mon Dec 16 10:04:12 1996 +0100
+++ b/src/Pure/NJ1xx.ML	Mon Dec 16 10:04:45 1996 +0100
@@ -127,3 +127,6 @@
      exportML (filename^".heap");
      print(banner^"\n")
   end;
+
+
+val needs_filtered_use = false;

--- a/src/Pure/POLY.ML	Mon Dec 16 10:04:12 1996 +0100
+++ b/src/Pure/POLY.ML	Mon Dec 16 10:04:45 1996 +0100
@@ -121,3 +121,7 @@
      close_in is;
      result
   end;
+
+
+
+val needs_filtered_use = true;