--- a/src/Pure/ML-Systems/polyml.ML Wed Dec 17 14:57:02 1997 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Wed Dec 17 14:57:26 1997 +0100
@@ -109,7 +109,7 @@
end;
-(* non-ASCII input (see also Thy/symbol_input.ML) *)
+(* non-ASCII input (see also Thy/use.ML) *)
val needs_filtered_use =
(case explode ml_system of
--- a/src/Pure/ML-Systems/smlnj-0.93.ML Wed Dec 17 14:57:02 1997 +0100
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML Wed Dec 17 14:57:26 1997 +0100
@@ -139,6 +139,6 @@
end;
-(* non-ASCII input (see also Thy/symbol_input.ML) *)
+(* non-ASCII input (see also Thy/use.ML) *)
val needs_filtered_use = false;
--- a/src/Pure/ML-Systems/smlnj.ML Wed Dec 17 14:57:02 1997 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Wed Dec 17 14:57:26 1997 +0100
@@ -117,6 +117,6 @@
| SOME txt => txt);
-(* non-ASCII input (see also Thy/symbol_input.ML) *)
+(* non-ASCII input (see also Thy/use.ML) *)
val needs_filtered_use = false;