[isabelle-dev] Additional type variable(s) in specification

[Tobias Nipkow]

Is the following behaviour really a good idea and useful?

inductive P :: "nat => bool" where
"P(suc n)"

is accepted but defines

P :: "'a itself => nat => bool"

It does kind of warn me by saying

### Additional type variable(s) in specification of P: 'a

but if you miss that warning, you will be very surprised about the kind
of errors you get later on when using P.

If I give a constant an explicit type, I would prefer Isabelle to
respect that.

Tobias