# HG changeset patch
# User wenzelm
# Date 1005260242 -3600
# Node ID b6f10dcde8037ff34afa86ea82c20a3c3cdf2a05
# Parent  16435c4e083f5b2020486642fce030eb2e5ce07c
removed needs_filtered_use;

diff -r 16435c4e083f -r b6f10dcde803 src/Pure/ML-Systems/mlworks.ML
--- a/src/Pure/ML-Systems/mlworks.ML	Thu Nov 08 23:55:04 2001 +0100
+++ b/src/Pure/ML-Systems/mlworks.ML	Thu Nov 08 23:57:22 2001 +0100
@@ -138,8 +138,3 @@
   (case OS.Process.getEnv var of
     NONE => ""
   | SOME txt => txt);
-
-
-(* non-ASCII input (see also Thy/use.ML) *)
-
-val needs_filtered_use = false;
diff -r 16435c4e083f -r b6f10dcde803 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Thu Nov 08 23:55:04 2001 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Thu Nov 08 23:57:22 2001 +0100
@@ -140,8 +140,3 @@
   (case Process.getEnv var of
     NONE => ""
   | SOME txt => txt);
-
-
-(* non-ASCII input (see also Thy/use.ML) *)
-
-val needs_filtered_use = false;
diff -r 16435c4e083f -r b6f10dcde803 src/Pure/ML-Systems/polyml-3.x.ML
--- a/src/Pure/ML-Systems/polyml-3.x.ML	Thu Nov 08 23:55:04 2001 +0100
+++ b/src/Pure/ML-Systems/polyml-3.x.ML	Thu Nov 08 23:57:22 2001 +0100
@@ -129,8 +129,3 @@
 
 
 end;
-
-
-(* non-ASCII input (see also Thy/use.ML) *)
-
-val needs_filtered_use = true;
diff -r 16435c4e083f -r b6f10dcde803 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Nov 08 23:55:04 2001 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Nov 08 23:57:22 2001 +0100
@@ -167,8 +167,3 @@
   (case OS.Process.getEnv var of
     NONE => ""
   | SOME txt => txt);
-
-
-(* non-ASCII input (see also Thy/use.ML) *)
-
-val needs_filtered_use = true;
diff -r 16435c4e083f -r b6f10dcde803 src/Pure/ML-Systems/smlnj-0.93.ML
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Thu Nov 08 23:55:04 2001 +0100
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Thu Nov 08 23:57:22 2001 +0100
@@ -220,8 +220,3 @@
   fun getenv var = drop_last_char
     (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
 end;
-
-
-(* non-ASCII input (see also Thy/use.ML) *)
-
-val needs_filtered_use = false;
diff -r 16435c4e083f -r b6f10dcde803 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Thu Nov 08 23:55:04 2001 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Nov 08 23:57:22 2001 +0100
@@ -206,8 +206,3 @@
   (case OS.Process.getEnv var of
     NONE => ""
   | SOME txt => txt);
-
-
-(* non-ASCII input (see also Thy/use.ML) *)
-
-val needs_filtered_use = false;