[isabelle] Quickcheck in locale with defines directive

Dear all,

Consider the following locale:

locale test =
  fixes foo :: "nat"
  defines "foo == 0"

  lemma "foo = 0" unfolding foo_def by rule


Isabelle2014 then produces this output at the lemma statement:

Auto Quickcheck found a counterexample:

foo = Suc 0

Evaluated terms:
0 = 0

So it looks like quickcheck thinks that it can still define "foo",
when it is actually already defined. Or did I misunderstand what the
defines directive does?

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.