# [isabelle] free term instantiations

Hello,
I was under the impression that all terms with free variables have
their terms instantiated (in full proof terms) in the order occurring in
the term. However, I happened upon the following counterexample:
which is instantiated
x, y,below,inf
instead of
below,inf,x,y
as a term order would indicate. Would someone please explain
the exact order of instantiation.
Thanks for your time (on this and previous questions),
Sean
Const ("==>", "prop => prop => prop") $
(Const ("Trueprop", "bool => prop") $
(Const
("Lattice_Locales.partial_order",
"('a => 'a => bool) => bool") $
Free ("below", "'a => 'a => bool"))) $
(Const ("==>", "prop => prop => prop") $
(Const ("Trueprop", "bool => prop") $
(Const
("Lattice_Locales.lower_semilattice_axioms",

` "('a => 'a => bool) => ('a => 'a => 'a)
``=> bool")
` $ Free ("below", "'a => 'a => bool") $
Free ("inf", "'a => 'a => 'a"))) $
(Const ("Trueprop", "bool => prop") $
(Const ("op =", "'a => 'a => bool") $

` (Free ("inf", "'a => 'a => 'a") $ Var (("x", 0),
``"'a") $
` Var (("y", 0), "'a")) $
(Free ("inf", "'a => 'a => 'a") $ Var (("y", 0), "'a") $
Var (("x", 0), "'a"))))) : Term.term
SOME (Var (("x", 0), "?'a")) %
SOME (Var (("y", 0), "?'a")) %
SOME (Var (("below", 0), "?'a => ?'a => bool")) %
SOME (Var (("inf", 0), "?'a => ?'a => ?'a")) %%
A more readable version (in HOL Light syntax) is:
Trueprop (lattice_locales_partial_order below)

` ==> Trueprop (lattice_locales_lower_semilattice_axioms
``below inf)
` ==> Trueprop (inf x y = inf y x)

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*