[isabelle-dev] Bad binding warnings

[Makarius]

On Thu, 14 Jul 2011, Lars Noschinski wrote:

> On 14.07.2011 21:20, Makarius wrote:
>> 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.
>
> Is it to be expected, that this warning now occurs quite often in a lemma 
> statement, even if Auto Quickcheck and Solve are disabled?

It is expected in the sense that the "more thorough" check of 9bd8d4addd6e 
should help to isolate boundary cases and sort them out.  See now 
1183951365de and 1c18d52204be.  More fine points are to be expected.

BTW, one of the oddities of the too liberal old scheme is the confusion 
caused by things like datatype foo = "nat * bool".  It was also possible 
to define constructors called "" or " " or "  " etc.


 	Makarius