# HG changeset patch
# User wenzelm
# Date 882367046 -3600
# Node ID 5c26253b8a2e99bfe835ec958b4f1dab403642ad
# Parent  6d4545f809e53927012f50daba8ca1692a878379
tuned comment;

diff -r 6d4545f809e5 -r 5c26253b8a2e src/Pure/ML-Systems/polyml.ML
--- 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
diff -r 6d4545f809e5 -r 5c26253b8a2e src/Pure/ML-Systems/smlnj-0.93.ML
--- 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;
diff -r 6d4545f809e5 -r 5c26253b8a2e src/Pure/ML-Systems/smlnj.ML
--- 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;