The classic method of Nelson and Oppen for combining decision procedures
requires the theories to be stably-infnite. 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, fxing 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.