[FOM] A question about AC in constructive mathematics

[Arnon Avron]

Recently I came across a theorem (and a proof) that 
AC implies the law of excluded middle in constructive
mathematics, implying that AC should be rejected
by intuitionists. I was surprised, since AC seems to me 
to be valid according to the BHK interpretation of the
logical constants, and is a indeed a theorem in Martin-Lö's 
intuitionistic type theoy.  Also Bishop wrote in his book 
that AC is valid from a constructive point of view.

 I'll be very grateful if one of the specialists here on FOM
clarifies this issue for me.

Thanks,

Arnon Avron