One of my papers did this for the existence of the maximal globally hyperbolic Cauchy development for the initial value problem in general relativity.

The TL;DR is that the original proof had a gratuitous use of Zorn's lemma. The fix is similar, but also somewhat different from, the fix removing the use of Zorn from maximal atlases.

One of my papers, A comment on the construction of the maximal globally hyperbolic Cauchy development, did this for the existence of the maximal globally hyperbolic Cauchy development for the initial value problem in general relativity.

The TL;DR is that the original proof had a gratuitous use of Zorn's lemma. The fix is similar, but also somewhat different from, the fix removing the use of Zorn from maximal atlases.