The classic method of Nelson and Oppen for combining decision procedures
requires the theories to be stably-infinite. Unfortunately, some important
theories do not fall into this category (e.g. the theory of bit-vectors). To
remedy this problem, previous work introduced the notion of *polite*
theories. Polite theories can be combined with any other theory using an
extension of the Nelson-Oppen approach. In this paper we revisit the notion of
polite theories, fixing a subtle flaw in the original definition. We give a new
combination theorem which specifies the degree to which politeness is preserved
when combining polite theories. We also give conditions under which politeness
is preserved when instantiating theories by identifying two sorts. These
results lead to a more general variant of the theorem for combining multiple
polite theories.