src/Pure/ML-Systems/smlnj-0.93.ML

   fun getenv var = drop_last_char
     (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
 end;
 
 
-(* non-ASCII input (see also Thy/symbol_input.ML) *)
+(* non-ASCII input (see also Thy/use.ML) *)
 
 val needs_filtered_use = false;