An algorithm for unification in equational theories