uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters); uniform treatment of target contexts as invisible; added Local_Theory.standard_form convenience;

tuned;

synchronize syntax uniformly for target stack and aux. context;