more careful treatment of set_context / reset_context for persistent morphisms; avoid persistent theory for eq_morphism / eq_term_morphism, notably in 'class' definition;

clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context; clarified signature;

tuned signature;