Dear Minhyong, 

I am quite happy with this isomorphism, but maybe not so much because of the proof using the axiom of choice (although I don't particularly object to AC) but rather because my sense is that, whenever this is used, what is *really* being used is a choice of isomorphism between
the algebraic closure of $\mathbb Q$ in $\mathbb C$ and the algebraic closure of $\mathbb Q$
in $\overline{\mathbb Q}_{\ell}$ (and I have absolutely no objection to identifying these two algebraic
closures).

Anytime one uses such an isomorphism in arithmetic, and it isn't ultimately being used to
identify algebraic numbers in the two fields, I think it is fairly meaningless.  (E.g., for modular forms of wt. $k \geq 1$, I am happy to identify the space over such over $\mathbb C$ with the analogous space over $\mathbb Q_{\ell}$, since the normalized cupsidal eigenforms have
algebraic integer coefficients, and so these spaces have a natural underlying $\overline{\mathbb Q}$-structure.  But to take non-algebraic Maass eigenforms, and to think of their Fourier coefficients as numbers in $\overline{\mathbb Q}_{\ell}$, while technically possible, is conceptually meaningless.)

In my own papers I often fix such an isomorphism (or even one for each $\ell$), but I don't think of it as having any significance beyond the identification of the two copies of
$\overline{\mathbb Q}$.