We give a fresh theoretical foundation for designing comprehensive solvers for satisfiability
modulo theories (SMT). In contrast with the traditional Nelson-Oppen approach dealing with 
theories in single- or multi-sorted first-order logic, we consider parametric theories---a 
restricted class of theories defined in the context of a higher-order logic with polymorphic 
types. Our main result is the combination theorem for decision procedures for disjoint 
parametric theories. Combinations of parametric theories conveniently express the "logic" of 
common datatypes, covering virtually all deeply nested structures (lists of arrays of sets of ...) 
that arise in verification practice. The vexatious stable infiniteness condition of the traditional 
approach is replaced in our setting with a milder flexibility condition. Our results do not 
subsume existing results, nor are subsumed by them, but they apply more widely because the 
datatypes relevant in applications are described by theories that satisfy our parametricity 
requirements without necessarily satisfying the stable infiniteness requirements of other 
combination methods.