I found this paper as a first result in Google after searching for "godel theorem proof".
On page 3:
Let $B_1(n), \,B_2(n), \,\dots$ be an enumeration of all formulas in $\mathcal{N}$ having exactly one free variable.
This seems fishy, can I really take one enumeration like this? Is this implicitly applying some form of the Axiom of Choice?
AC is not required for this. We know there is an enumeration (i.e. the set of all enumerations is nonempty), so we can consider one. This is only one arbitrary choice, not an infinite number, so AC is not required.
(One situation where choice is sometimes necessary but easy to overlook is when we need to define an infinite sequence of enumerations of countable sets. For instance, this occurs in the usual proof that a countable union of countable sets is countable, which is a theorem that cannot be proved without countable choice. However, in this question we are only considering one, not an infinite number of enumerations.)
Moreover, here, we can actually define an explicit enumeration of formulas constructively, for instance by assigning each symbol a natural number, and then using the dictionary order on the finite sequences of natural numbers and going through all of these sequences, picking out in order the ones that represent formulae with one variable.