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

[Brian Huffman]

On Thu, Dec 2, 2010 at 8:42 AM, Makarius <makarius at sketis.net> wrote:
> 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.

Making the warning message more visible is only a partial solution.
The wording of the warning itself is also a problem:

"Additional type variable(s) in specification"

Users who encounter this warning because of a mistake in a definition
are unlikely to know what it means (unless they have read about it on
the mailing list). More importantly, the warning message doesn't give
any hints about how to fix the mistake.

- Brian