In the proof of Trakhtenbrot's theorem (as given in "Elements of Finite Model Theory" by Leonid Libkin), for every Turing machine $M$, author constructs a FO sentence $\Phi_M$ of vocabulary $\sigma$ such that $\Phi_M$ is finitely satisfiable iff $M$ halts on the empty input. Then he says that as the latter is known to be undecidable so the theorem holds.
My doubt is, the vocabulary $\sigma$ that was constructed depends on the Turing Machine $M$. But the theorem holds for any relational vocabulary with at least one binary relation symbol and also it should not depend on the machine $M$. Perhaps the claim of author is enough to imply the theorem for arbitrary vocabulary, but I am unable to see how.