Right now I am reading a proof of Downward Löwenheim-Skolem theorem in Hodges, but I am slightly confused about a proof Hodges makes. Let me write down some of the definitions.

Definition: Let $T$ be a first-order theory in a first-order language $\scr{L}$. >Then a skolemisation of $T$ is a theory $T^+\supseteq T$ in a first order >language $\scr{L}^+\supseteq \scr{L}$ such that

1. Any model of $T$ can be expanded to a model of $T^+$.
2. For every formula $\phi(\bar{x}, y)$ of $\scr{L}^+$ with $\bar{x}$ a nonempty tuple, there is a term $t$ of $\scr{L}^+$ such that $$T^+\vdash \forall \bar{x}(\exists y\phi(\bar{x}, y)\to \phi(\bar{x}, t(\bar{x}))).$$

A theory $T$ is said to be a Skolem Theory or to have Skolem functions if $T^+:=T$ and $\scr{L}^+ = \scr{L}$ is a skolemisation of $T$, i.e. $T$ is a skolemisation of itself.

Hodges goes on to say that for a Skolem theory $T$, and $A$ a model of $T$ and $X$ a subset of $A$, if the skolem hull $B:=\langle X\rangle_A$ is nonempty, then it is an elementary substructure of $A$. He proves this by invoking the Tarski-Vaught Criterion for elementary substructures. In particular, if $\phi(\bar{x}, y)$ is a $\scr{L}$-formula and $\bar{a}$ is a tuple from $B$ with $A\models \exists y \phi(\bar{a}, y)$, then $A\models \phi(\bar{a}, t(\bar{a}))$ for the appropriate term $t$. But $t^A(\bar{a})\in B$ as $B$ is closed under the functions, and he concludes that $B$ satisfies the Tarski-Vaught Criterion and so $B\preceq A$.

Here is my question, what if $\phi(\bar{x}, y)$ is actually $\phi(y)$? Then $\exists y\phi(y)$ is a sentence and so does not have a Skolem function. So if $A\models \exists y\phi$, how can we guarantee that $B$ possesses a witness to $\exists y\phi$?

My attempt to work around this is to consider the formula $$\psi(x, y): = \ulcorner \phi(y)\wedge x=x\urcorner.$$ Then $\exists y\phi(y)$ is logically equivalent to $\exists y \psi(x, y)$. As $T$ is a skolem theory, there is a term $t(x)$ such that $$T\vdash \forall x(\exists y\psi(x, y)\to \psi(x, t(x))).$$ Then for any $a\in B$, $t^A(a)$ will be an element of $B$ witnessing $A\models \exists y\phi$. Is this a correct resolution of my question, or is there something else I am missing? Thanks for the help!

Yes, your solution works. A less "cheap" way to resolve things is to remove the word "nonempty" from Hodges' definition, so that $(\exists y)\phi(y)$ has a zero-ary Skolem function, that is, a "Skolem constant" $c_\phi$. That is the definition of a Skolemization some others use. (I am not familiar with Hodges' definitions and conventions; he might not require that a variable shown in a formula name must actually appear, in which case he could write "$(\exists y)[y = y]$" as $\phi(x)$.)