[isabelle] Better way to beta apply two terms



Hi,

What is a better way to beta-apply two terms without using betapply, which
can cause a type mismatch. For example:

consts
a :: nat
F :: "'a => nat"
ML {*
val ftrm = @{term "F"};
val atrm = @{term "a"};
val res = betapply((ftrm,atrm));
type_of res
*}

The application succeeds, but the resulting term isn't well-typed (thus
type_of fails). betapply doesn't seem to change the input type of F from a
variable to "Nat.nat". Is there a better way of beta applying such that the
input type can automatically be updated?

Thanks for the help in advance!

Steve




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