# [isabelle] Constructing terms in ML

Hi all,
I'm trying to construct the term for "ALL x y. x = y". I know I could just
use Syntax.read_term, but what if I want to construct it term by term using
the constructor functions? I see that the term should look something like:
Const ("HOL.All", "('a => HOL.bool) => HOL.bool") $
Abs ("x", "'a",
Const ("HOL.All", "('a => HOL.bool) => HOL.bool") $
Abs ("y", "'a",
Const ("HOL.eq", "'a => 'a => HOL.bool") $ Bound 1 $ Bound 0))
Without fixing the types of x and y, HOLogic.mk_eq (Bound 0, Bound 1) gives
an error, because it can't find the type of Bound terms. I was just thinking
to create the mk_eq term first, then wrap it inside a mk_all and itself
inside another mk_all. Is there a better way to go about this?
Thanks a lot in advance.
Steve

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