The Wikipedia page on the compactness theorem says:
One of those proofs relies on ultraproducts hinging on the axiom of choice as follows:
Proof: Fix a first-order language $L$, and let $\Sigma$ be a collection of $L$-sentences such that every finite subcollection of $L$-sentences, $i\subseteq\Sigma$ of it has a model ${\displaystyle {\mathcal {M}}_{i}}$.
Is the axiom of choice already used here? As an hypothesis, we assume that for each $i$, there is a model $A\models i$. Do we need the axiom of choice here to fix for each $i$ one such specific model $\mathcal M_i$?