Question about the proof of Theorem 3.1.4 in Marker's Model Theory, An Introduction On page 73 of Marker's Model Theory, An Introduction the following theorem can be found:
Theorem 3.1.4 Suppose that $L$ contains a constant symbol $c$, $T$ is an $L$-theory, and $\varphi ( \bar v)$ is an $L$-formula. The following are equivalent:
i) There is a quantifier-free $L$-formula $\psi ( \bar v )$ such that $T \models \forall \bar v \, ( \varphi (\bar v) \leftrightarrow \psi (\bar v) )$.
ii) If $M$ and $N$ are models of $T$, $A$ is an $L$-structure, $A \subseteq M$, and $A \subseteq N$, then $M \models \varphi (\bar a)$ if and only if $N \models \varphi (\bar a)$ for all $\bar a \in A$. 
The proof of i) $\Rightarrow$ ii) is easy.
To show ii) $\Rightarrow$ i), Marker makes a case distinction. He first supposes $T \models \forall \bar v \, \varphi ( \bar v )$: then $T \models \forall \bar v \, ( \varphi (v) \leftrightarrow c = c )$, so we're done. Similarly if $T \models \forall \bar v \, \neg \varphi ( \bar v )$, then we're done because $T \models \forall \bar v \, ( \varphi (v) \leftrightarrow c \neq c )$.
After that, he states: Thus, we may assume that both $T ∪ \{\varphi (\bar v)\}$ and $T ∪ \{\neg \varphi (\bar v)\}$ are satisfiable. Of course, I agree with this statement - this is not an issue.
My problem lies in the fact that in the subsequent proof that Marker gives it is not at all clear to me where this assumption is used. (Note that at no spot he explicitly mentions the usage of this assumption.)
So my concrete question is: where is this assumption used in Marker's proof?
I think it should be used somewhere, otherwise it seems that the assumption the language have at least one constant can be omitted from the statement. 
(NB: Alas, the complete proof is a little lengthy to post here.)
 A: Marker is rather messy on this point. It is a minor point (that is why nobody cares) but it may confuse students.
When Marker defines formulas he forgets a connective: the 0-ary Boolean connective $\top$ (or $\bot$, if you prefer). The role of this connective is merely formal: it allows you to write a quantifier-free sentence also in languages without constants. 
You need to have it otherwise relational theories (e.g. dense linear orders, random graphs) would never have elimination of quantifiers for a trivial reason: there is no quantifier-free sentence equivalent to $\forall x\ (x=x)$.
A: See proof page 74; Marker wants to prove the Claim : 

$T \cup \Gamma(\overline d) \vDash \phi(\overline d)$.

He proceeds by contradiction, assuming : $\mathcal M \vDash T \cup \Gamma(\overline d) \cup \{ \lnot \phi(\overline d) \}$.
This, I think, is the point ... If one of $T \cup \{ \phi(\overline v) \}$ or $T \cup \{ \lnot \phi(\overline v) \}$ were unsatisfiable, "adding" to $T$ the new premises $\Gamma$ will not change this situation.
