warn_obsolete for goal commands -- danger of disrupting a local proof context; Goal.init, Goal.conclude, Goal.norm_hhf_rule; shortcuts no longer pervasive (cf. structure OldGoals);