[Python-Dev] Alternative name for str.partition()