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

[Makarius]

On Thu, 2 Dec 2010, John Matthews wrote:

> As another user data point, a few months back I ran into this same issue 
> of the type I specified not being the type Isabelle gave me back. It was 
> pretty confusing at the time and it took me a while to figure out what 
> was going on.

Sorry, I don't quite get it.

What you specify is a type constraint for the main body of the 
specification text.  There can be a mismatch of what the system infers as 
most general type and what you've had in mind.  There can be also 
surprises due to type abbreviations.

Which situation did you have exactly?


 	Makarius