removed needs_filtered_use;
authorwenzelm
Thu Nov 08 23:57:22 2001 +0100 (2001-11-08)
changeset 12108b6f10dcde803
parent 12107 16435c4e083f
child 12109 bd6eb9194a5d
removed needs_filtered_use;
src/Pure/ML-Systems/mlworks.ML
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml-3.x.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj-0.93.ML
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/src/Pure/ML-Systems/mlworks.ML	Thu Nov 08 23:55:04 2001 +0100
     1.2 +++ b/src/Pure/ML-Systems/mlworks.ML	Thu Nov 08 23:57:22 2001 +0100
     1.3 @@ -138,8 +138,3 @@
     1.4    (case OS.Process.getEnv var of
     1.5      NONE => ""
     1.6    | SOME txt => txt);
     1.7 -
     1.8 -
     1.9 -(* non-ASCII input (see also Thy/use.ML) *)
    1.10 -
    1.11 -val needs_filtered_use = false;
     2.1 --- a/src/Pure/ML-Systems/mosml.ML	Thu Nov 08 23:55:04 2001 +0100
     2.2 +++ b/src/Pure/ML-Systems/mosml.ML	Thu Nov 08 23:57:22 2001 +0100
     2.3 @@ -140,8 +140,3 @@
     2.4    (case Process.getEnv var of
     2.5      NONE => ""
     2.6    | SOME txt => txt);
     2.7 -
     2.8 -
     2.9 -(* non-ASCII input (see also Thy/use.ML) *)
    2.10 -
    2.11 -val needs_filtered_use = false;
     3.1 --- a/src/Pure/ML-Systems/polyml-3.x.ML	Thu Nov 08 23:55:04 2001 +0100
     3.2 +++ b/src/Pure/ML-Systems/polyml-3.x.ML	Thu Nov 08 23:57:22 2001 +0100
     3.3 @@ -129,8 +129,3 @@
     3.4  
     3.5  
     3.6  end;
     3.7 -
     3.8 -
     3.9 -(* non-ASCII input (see also Thy/use.ML) *)
    3.10 -
    3.11 -val needs_filtered_use = true;
     4.1 --- a/src/Pure/ML-Systems/polyml.ML	Thu Nov 08 23:55:04 2001 +0100
     4.2 +++ b/src/Pure/ML-Systems/polyml.ML	Thu Nov 08 23:57:22 2001 +0100
     4.3 @@ -167,8 +167,3 @@
     4.4    (case OS.Process.getEnv var of
     4.5      NONE => ""
     4.6    | SOME txt => txt);
     4.7 -
     4.8 -
     4.9 -(* non-ASCII input (see also Thy/use.ML) *)
    4.10 -
    4.11 -val needs_filtered_use = true;
     5.1 --- a/src/Pure/ML-Systems/smlnj-0.93.ML	Thu Nov 08 23:55:04 2001 +0100
     5.2 +++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Thu Nov 08 23:57:22 2001 +0100
     5.3 @@ -220,8 +220,3 @@
     5.4    fun getenv var = drop_last_char
     5.5      (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
     5.6  end;
     5.7 -
     5.8 -
     5.9 -(* non-ASCII input (see also Thy/use.ML) *)
    5.10 -
    5.11 -val needs_filtered_use = false;
     6.1 --- a/src/Pure/ML-Systems/smlnj.ML	Thu Nov 08 23:55:04 2001 +0100
     6.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Thu Nov 08 23:57:22 2001 +0100
     6.3 @@ -206,8 +206,3 @@
     6.4    (case OS.Process.getEnv var of
     6.5      NONE => ""
     6.6    | SOME txt => txt);
     6.7 -
     6.8 -
     6.9 -(* non-ASCII input (see also Thy/use.ML) *)
    6.10 -
    6.11 -val needs_filtered_use = false;