[isabelle] Type unification failed



Hi,

Does anyone know why there's a type error in

ML {*
val trm = @{term "(f::'a=>nat) (a::nat)"};
*}

but not in

consts
f:: "'a => nat"
a :: nat

ML {* @{term "f a" *}

Why are the two cases treated differently?

Thanks

John




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