Efficiency of unification

Unification is trying to hard to unify things which are never going to
work, and backtracking a lot. This stops that.
Fixes #1219