# HG changeset patch
# User wenzelm
# Date 850727085 -3600
# Node ID acddf41dbbf76ed048b6735f1fdb0f4058a8dd73
# Parent  f733d555b3d041c2568c3c6d44ab1413852d803f
added needs_filtered_use;

diff -r f733d555b3d0 -r acddf41dbbf7 src/Pure/ML-Systems/polyml.ML
--- 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);
diff -r f733d555b3d0 -r acddf41dbbf7 src/Pure/ML-Systems/smlnj-1.09.ML
--- 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;
diff -r f733d555b3d0 -r acddf41dbbf7 src/Pure/NJ093.ML
--- 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;
diff -r f733d555b3d0 -r acddf41dbbf7 src/Pure/NJ1xx.ML
--- 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;
diff -r f733d555b3d0 -r acddf41dbbf7 src/Pure/POLY.ML
--- 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;