Let E be a first-order equational theory. A translation of higher-orde
r E-unification problems into a combinatory logic framework is present
ed and justified. The case in which E admits presentation as a converg
ent term rewriting system is treated in detail: in this situation, a m
odification of ordinary narrowing is shown to be a complete method for
enumerating higher-order E-unifiers. In fact, we treat a more general
problem, in which the types of terms contain type variables.