An Algorithm for Unification in Equational Theories