Injectives and choice

Grothendieck's proof that every AB5 category has enough injectives uses the axiom of choice (actually Zorn's lemma--which John Bell points out to me is significantly weaker than choice in toposes). And the proof in Johnstone's TOPOS THEORY that the category of Abelian groups over any Grothendieck topos has enough injectives uses Barr's theorem: Every Grothendieck topos is covered by one that satisfies the axiom of choice. This theorem itself assumes the axiom of choice in the base topos (i.e. the one over which the others are Grothendeick). Are there any good results showing how necessary the axiom of choice, or Zorn's lemma, is to these results?