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

[Makarius]

On Thu, 2 Dec 2010, Tobias Nipkow wrote:

> Florian explained to me that for the function package this new behaviour 
> is an improvement, but that does not mean that unsuspecting users should 
> be subjected to it.

Maybe Florian (and Alex) can post again the concrete examples they were 
mentioning to me 1 or 2 years ago.

As usual with the locale and locale theory specification business, the 
situation is a bit more complex than most people think.  The version of 
09e238561460 is one more step towards *less* surprise in this notoriously 
difficult issue of hidden polymorphism.  The same technique of itself 
abstractions is used in several other parts of the system, too.

Right now there is already a clear warning -- which Proof General happens 
to show in a hardly visible way, but that is just one of many problems of 
Proof General.  In Isabelle/jEdit the warning is hard to miss. I will 
check again about the other related messages to increase the pontential 
further.


 	Makarius