more accurate context;

reactivate Thm.check_hyps, after adapting AFP/Datatype_Order_Generator (see AFP/b7e389b5765c);

check_hyps for attribute application (still inactive, due to non-compliant tools); bypass check_hyps for locale expressions, where assumptions are not necessarily declared in intermediate situations;