Question

I described an example, Hindman's theorem, at http://mathoverflow.net/questions/94546 . The short version is that Hindman's original proof was unpleasantly complicated, whereas a later proof by Galvin and Glazer is now accepted as the standard proof. On the intuitive level, it's a definite improvement. Formally, though, from the viewpoint of reverse mathematics, Hindman's original proof is "better" because it uses far weaker set-existence assumptions.