1.1 --- a/src/Pure/ML-Systems/polyml.ML	Wed Dec 17 14:57:02 1997 +0100
     1.2 +++ b/src/Pure/ML-Systems/polyml.ML	Wed Dec 17 14:57:26 1997 +0100
     1.3 @@ -109,7 +109,7 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -(* non-ASCII input (see also Thy/symbol_input.ML) *)
     1.8 +(* non-ASCII input (see also Thy/use.ML) *)
     1.9  
    1.10  val needs_filtered_use =
    1.11    (case explode ml_system of

     2.1 --- a/src/Pure/ML-Systems/smlnj-0.93.ML	Wed Dec 17 14:57:02 1997 +0100
     2.2 +++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Wed Dec 17 14:57:26 1997 +0100
     2.3 @@ -139,6 +139,6 @@
     2.4  end;
     2.5  
     2.6  
     2.7 -(* non-ASCII input (see also Thy/symbol_input.ML) *)
     2.8 +(* non-ASCII input (see also Thy/use.ML) *)
     2.9  
    2.10  val needs_filtered_use = false;

     3.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Dec 17 14:57:02 1997 +0100
     3.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Dec 17 14:57:26 1997 +0100
     3.3 @@ -117,6 +117,6 @@
     3.4    | SOME txt => txt);
     3.5  
     3.6  
     3.7 -(* non-ASCII input (see also Thy/symbol_input.ML) *)
     3.8 +(* non-ASCII input (see also Thy/use.ML) *)
     3.9  
    3.10  val needs_filtered_use = false;