collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);

more uniform group for map_future, which is relevant for cancel in worker_task vs. future_job -- prefer peer group despite 81d03a29980c;

tuned message;

tuned comment;