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.