# [isabelle] Problem with overloading and inductive

Hallo,
I have a problem when I try to use a overloaded function in a
inductive definition. I've made a small example to illustrate that:
consts lifu :: "'a => 'b"
overloading lifu1 == "lifu::'a list => int"
lifu2 == "lifu::int => nat"
begin
definition lifu1 where "lifu1 == length"
definition lifu2 where "lifu2 == nat"
end
inductive ind_lifu :: "int list => int => bool"
where
base: "lifu (a::int list) = lifu (b::int) ==> ind_lifu a b"
If i try to give that to Isabelle/HOL, i get the message:
Specification depends on extra type variables: "'a::{}"
Did I do something wrong or is this a bug?
Thanks,
Christoph Feller

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