There are indeed many proofs of the Compactness theorem. As
I mention in [this MO
answer](http://mathoverflow.net/questions/9309/in-model-theory-does-compactness-easily-imply-completeness/9317#9317),
my graduate experience was with Leo Harrington, who
announced to the class that he used a different proof
method for Compactness each time he taught the introductory
graduate logic course in Berkeley. I am not sure for how
many semesters he was able to keep this up, but when I had
him, it was time for the Boolean-valued models proof.

The [Compactness
Theorem](http://en.wikipedia.org/wiki/Compactness_theorem)
is the assertion that if a first order theory $T$ is
finitely satisfiable (all finite subtheories have a model),
then $T$ itself is satisfiable.

Let me describe a number of proofs.

 - Goedel's original proof was via the [Completeness
 theorem](http://en.wikipedia.org/wiki/Completeness_theorem), deducing it as a trivial corollary. If $T$ is
 inconsistent, then the proof of a contradiction is finite,
 so there is an inconsistent finite subtheory. This proof
 is deprecated by contemporary logicians, because the Compactness theorem
 lies completely on the semantic side of the syntax/semantic divide,
 and it seems beside the point to have to develop the
 entire syntactic theory of formal proofs and derivations
 in order to make a conclusion purely about the semantic notions of
 models and satisfiability.

 - The Henkin proof. The point is that the usual Henkin
 proof of the Completeness theorem also serves directly to prove the
 Compactness theorem. Suppose that every finite subset of
 $T$ is satisfiable. By the usual details of the Henkin argument, we may extend $T$ to a
 finitely-satisfiable complete consistent Henkin theory
 $T^+$, in a language with new constant symbols (using the
 theorem on constants). That is, the new theory contains
 the Henkin assertions $\exists x\varphi(x)\to \varphi(c)$,
 where $c$ is a new constant symbol added for this purpose with
 $\varphi$. Now, from $T^+$ we may build a
 model out of the Henkin constants in the usual manner.
 The reduct of this model to the original language
 satisfies $T$, as desired.

 - The proof via Skolem functions (as you requested). This
 amounts basically just to a more complicated version of the Henkin
 proof. I recall Henkin giving a talk at the Berkeley Logic
 Colloquium in which he explained that the idea for his
 proof of the Completeness theorem arose to him in a dream, after
 considering the (at that time standard) Skolem function
 proof of Completeness. The
 point was that in that proof, one adds Skolem functions to
 the language to tie the formula $\varphi(x)$ to the
 witness $f_\varphi(x)$, so that one adds the formulas
 $\exists x\varphi(x)\to \varphi(f_\varphi(x))$, instead of
 the Henkin assertion. But otherwise, it works out
 similarly---one proves the analogue of the theorem on constants that
 allows one to add the Skolem function assertions, and then
 builds the model out of formal term expressions. Henkin said that he
 realized in his dream that there was no
 need to tie the witness so closely to the formula with the
 Skolem function, and that merely having the presence of a
 constant to serve as a witness sufficed. Thus was born the
 Henkin proof.

 - The ultrapower proof. Pete has an explanation of this proof in his
 answer. If $T$ is finitely satisfiable, then consider the
 set of finite subsets $t\subset T$, each of which has a model
 $M_t\models t$. Let $F$ be an ultrafilter
 containing for each $\varphi\in T$ the set of finite $t\subset
 T$ with $\varphi\in t$, a collection with the finite
 intersection property. The ultrapower of $\Pi_t M_t/F$
 satisfies every $\varphi\in T$ by \L os's theorem.

 - The reduced product proof. In this proof, one first
 develops the concept of a reduced product $\Pi_t M_t/F_0$,
 where $F_0$ is only a filter instead of an ultrafilter (the filter
 generated by the collection with FIP above).
 And then you can finish the job by considering a quotient
 of this structure, which essentially amounts to the
 ultraproduct.

 - The Boolean-valued model proof. It is similar to the ultrapower
 proof and the reduced power proof (they are all essentially the same),
 but there is no need to
 quotient out by $F$ in
 advance. Instead, one builds a $\mathbb{B}$-valued model
 out of the product ${\cal M}=Pi_t M_t$, where $\mathbb{B}$ is the Boolean algebra
 of all subsets of finite subsets of $T$, so that the truth-value of a statement $\varphi$
 in $\cal M$ is the set of $t$ for which $M_t\models
 \varphi$. Then, one develops the general theory allowing one to quotient a
 Boolean-valued model by a filter, and the conclusion
 amounts to \L os in the ultrapower proof.