[isabelle-dev] Bad binding warnings

[Lars Noschinski]

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
   Plain
begin

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

end
---------------

   -- Lars