Before revision: (And since any weaker inference you can get is a substitution instance of the most general one, nothing less than the most general unifier is ever used in practice.
After revision: Since any weaker inference you can get is a substitution instance of the most general one, nothing less than the most general unifier is ever used in practice.