[polyml] Apparent bug in String.tokenize