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