Mathematical reasoning often involves defining non-trivial sets and relations. In Higher-Order Logic, this is reflected by the fact that instantiating a quantifier can change the logical structure of a formula. This complicates proof search since we cannot rely solely on unification for instantiations. I have recently developed a technique for combining theorem proving with generating and solving set constraints. This is implemented in the Higher-Order theorem prover TPS.