[isabelle-dev] Bad binding warnings

Lars Noschinski noschinl at in.tum.de
Thu Jul 14 22:53:38 CEST 2011

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? E.g. 
the following theory triggers it, but only in interactive mode:

theory Scratch imports

   fixes A :: 'a
   assumes "P A"
   shows "Q"


   -- Lars

More information about the isabelle-dev mailing list