[isabelle] Problem with overloading and inductive


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"
definition lifu1 where "lifu1 == length"
definition lifu2 where "lifu2 == nat"

inductive ind_lifu :: "int list => int => bool"
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?

Christoph Feller

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