Unify handling of type abbrevs and type operators

This is analogous to what is done with terms, where the handling of
genuine constants passes through the overload map.

The main desirable effect should be that if multiple genuine type
operators with the same name are in the grammar, then only one will
print unqualified; all the others will print with theory-qualification.

Currently fails in src/datatype's selftest as ParseDatatype doesn't see
bare names that are existing types as possible occurrences of recursive
types.

Fixes and tests arising from namespacing tyabbrevs

Document how to remove/disable-printing-for all type abbreviations of a
given name, or a specific abbreviation from a given theory.

Tests for this. Final cleanup for #168 I hope.