# HG changeset patch # User wenzelm # Date 957779147 -7200 # Node ID 3e95f3a90875248fac24e4baa87ba8bd5196e83d # Parent d93e235837a97b0ccb44f14248f9c0b99b4eb8b4 val needs_filtered_use = true; diff -r d93e235837a9 -r 3e95f3a90875 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Mon May 08 11:35:19 2000 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Mon May 08 11:45:47 2000 +0200 @@ -134,7 +134,4 @@ (* non-ASCII input (see also Thy/use.ML) *) -val needs_filtered_use = - (case explode ml_system of - "p" :: "o" :: "l" :: "y" :: "m" :: "l" :: "-" :: "3" :: _ => true - | _ => false); +val needs_filtered_use = true;