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