Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)

Mathematicians sometimes worry about the Axiom of Choice (AC) and Axiom of Determinancy (AD). Axiom of Choice: Given any collection ${\cal C}$ of nonempty sets, there is a function $f$ that, given a set $S$ in ${\cal C}$, returns a member of $S$. Axiom of Determinacy: Let $S$ be a set of infinitely long bit strings. Alice and Bob play a game where Alice picks a 1st bit $b_1$, Bob picks a 2nd bit $b_2$, and so on, until an infinite string $x = b_1 b_2 \cdots $ is constructed. Alice wins the game if $x \in S$, Bob wins the game if $x \not \in S$. The assumption is that for every $S$, there is a winning strategy for one of the players. (For example, if $S$ consists only of the all-ones string, Bob can win in finitely many moves.) It is known that these two axioms are inconsistent with each other. (Think about it, or go here.) Other mathematicians pay little or no attention to the use of these axioms in a proof. They would seem to be almost irrelevant to theoretical computer science, since we believe that we work mostly with finite objects. However, because TCS defines computational decision problems to be infinite bit strings, and we measure (for example) the time complexity of an algorithm as an asymptotic function over the naturals, there is always a possibility that the usage of one of these axioms could creep into some proofs. What is the most striking example in TCS that you know where one of these axioms are required? (Do you know any examples?) Just to foreshadow a bit, note that a diagonalization argument (over the set of all Turing machines, say) is not an application of the Axiom of Choice. Although the language that a Turing machine defines is an infinite bit string, each Turing machine has a finite description, so we really don't require a choice function for infinitely many infinite sets here. (I put a lot of tags because I have no idea where the examples will come from.)