What are the essential uses of built-in Skolem functions in model theory?

Question

Built-in Skolem functions are often used to present classical results in model theory in textbooks. However, I noticed that the use of built-in Skolem function can often be avoided. The following are some examples:

1. Loewenheim-Skolem theorems. Having names for the Skolem functions is useful but not necessary; one just has to be careful in adding points to your model.
2. Quantifier elimination. The so-called Morleyization, i.e., naming each definable subsets by a new relation symbol, suffices.
3. Ehrenfeucht-Mostowski models. There seems to be a way around since in continuous logic the existence of indiscernibles is proved without built-in Skolem functions, I'm told. (This is actually the motivation for this question.)

Hence, my question is: what are the essential uses of built-in Skolem functions in model theory?

Answer 1

While it is true that you can almost always get around the Skolem function issue in continuous logic, either by using a different method or by literally discretizing the structure in question (see the discussion in this paper for instance), there is one thing you can prove with Skolem functions in discrete logic that I do not know how to generalize to continuous logic (which I originally discussed in an answer to a MathOverflow question here):

Is it true that every complete continuous theory $T$ can be extended by definable predicates and functions to a theory $T'$ that is axiomatized by universal sentences?

As I mention in my other answer, however, I believe this question is equivalent to asking whether every continuous theory can be Skolemized in the traditional sense (i.e., expanded by definable functions in such a way that every substructure is an elementary substructure), so this may be a slightly circular answer.