clarified Future.map (again): finished value is mapped in-place, which saves task structures and changes error behaviour slightly (tolerance against canceled group of old value etc.);

back to polyml-5.4.1 (cf. b3110dec1a32) -- no cause of spurious interrupts;

merged

back to parallel HOL-BNF-Examples, which seems to have suffered from Future.map on canceled persistent futures;

more basic Goal.reset_futures as snapshot of implicit state; more robust Session.finish_futures: do not cancel here, to allow later Future.map of persistent futures (notably proof terms);

tuned proof;