[isabelle-dev] Bad binding warnings

[Makarius]

On Thu, 14 Jul 2011, Lukas Bulwahn wrote:

> Working with the development version, I have been noticing warnings "... 
> Bad binding: ...". Is there now a stricter guideline using or creating 
> bindings that Isabelle's developers should follow?

Not "now", they have been there for several years already.  Formal 
entities within the term language need to observe proper identifier 
syntax.  I cannot quote the many problems with totally arbitrary names on 
the spot, because it is such a long time ago when this was still done 
routinely (like global constants "op +" or "op *").

Recently I've noticed that internal "fixes" where accidentally omitted 
from the binding check.  There were also some incidents and genuine 
programming errors introduced due to the absence of a proper check.

For example, Variable.add_fixes with type variables 'a 'b etc. simply does 
not make any sense.  Now you get a warning at least.  See also the 
somewhat compact explanation of type variables vs. term variables in in 
the implementation manual section 5.1.


 	Makarius