Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed needs_filtered_use;
authorwenzelm
Thu, 08 Nov 2001 23:57:22 +0100
changeset 12108 b6f10dcde803
parent 12107 16435c4e083f
child 12109 bd6eb9194a5d
removed needs_filtered_use;
src/Pure/ML-Systems/mlworks.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/mosml.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/polyml-3.x.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/polyml.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/smlnj-0.93.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/smlnj.ML file | annotate | diff | comparison | revisions 
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
isabelle