1.1 --- a/src/Pure/ML-Systems/polyml.ML	Mon May 08 11:35:19 2000 +0200
     1.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon May 08 11:45:47 2000 +0200
     1.3 @@ -134,7 +134,4 @@
     1.4  
     1.5  (* non-ASCII input (see also Thy/use.ML) *)
     1.6  
     1.7 -val needs_filtered_use =
     1.8 -  (case explode ml_system of
     1.9 -    "p" :: "o" :: "l" :: "y" :: "m" :: "l" :: "-" :: "3" :: _ => true
    1.10 -  | _ => false);
    1.11 +val needs_filtered_use = true;