prefer plain Attrib.eval_thmss -- also means the assert_forward of Proof.get_thmss_cmd is skipped, leading to uniform (albeit odd) behaviour concerning forward chaining; tuned;

prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;

tuned eval_thms (cf. note etc. in proof.ML);

use Pretty.enum convenience;

tuned whitespace;

more precise and more maintainable dependencies;

merged, resolving conflict in src/Pure/IsaMakefile concerning General/xml_data.ML;