  This paper provides an effective uniform rate of metastability (in the sense
of Tao) on the strong convergence of Halpern iterations of nonexpansive
mappings in CAT(0) spaces. The extraction of this rate from an ineffective
proof due to Saejung is an instance of the general proof mining program which
uses tools from mathematical logic to uncover hidden computational content from
proofs. This methodology is applied here for the first time to a proof that
uses Banach limits and hence makes a substantial reference to the axiom of
choice.
