  Geometric theories based on classical logic are conservative over their
intuitionistic counterparts for geometric implications. The latter result
(sometimes referred to as Barr's theorem) is squarely a consequence of
Gentzen's Hauptsatz. Prima facie though, cut elimination can result in
superexponentially longer proofs. In this paper it is shown that the
transformation of a classical proof of a geometric implication in a geometric
theory into an intuitionistic proof can be achieved in feasibly many steps.
