Summary
- merged
- tuned signature;
- tuned signature;
- tuned signature;
- removed unused clone of (map o apsnd); removed unused variant of HOLogic.mk_obj_eq;
- prefer existing HOLogic.mk_obj_eq, despite subtle semantic differences of COMP vs. RS;
- added HOLogic.mk_obj_eq convenience and eliminated some clones;
- tuned -- use existing Morphism.instantiate_morphism;