I believe this is an issue in general logic, not specific to HOL,
and revolves about the implementation of schemata such as Comprehension.
Consider (2) first: It is a general fact of logic that adding a Skolem
function is conservative. It doesn't matter whether there are additional
free variables. Thus, say T is some axiomatic theory and P(y,z,x) is
some predicate in the language of T. You may add a new function symbol,
f, and add a new axiom to the theory:
forall y z [(exists x P(y,z,x)) --> P(y,z f(y,z))] (*)
Then, if phi is some sentence in the original language of T and phi
is provable from T + (*), then phi is provable from T alone.
In particular, phi could be AC (say, "every set can be well-ordered"),
if T is some sort of set theory or type theory in which the relevant
notions can be expressed.
BUT, if T is set theory, you have to be careful that
the Comprehension schema be used only with formulae from the original
language. If you extend Comprehension to involve formulae in f,
you will derive AC -- the extension is no longer conservative.
BUT, there are two situations in which the extension is still conservative,
even if you extend Comprehension to involve formulae in f:
a: Situation (1): where it is provable from T that for each y,z,
there is no more than one x satisfying P(y,z,x). Then each
formula in f is equivalent to a formula without f, so Comprehension
with formulae in f is still conservative.
b: P has no free variables other than x, so f is a Skolem constant.
This is OK because the Comprehension schema allows an arbitrary
number of fixed parameters.
Ken Kunen