[isabelle-dev] [isabelle] Confusing behavior of a paired set comprehension

[Tobias Nipkow]

Am 04/04/2012 11:48, schrieb Tjark Weber:
> Adhering to the principle of least astonishment, I suspect an error
> message (or at least a warning) would be more helpful.

Isabelle's well-tried principle of least astonishment is not to give too many
helpful error messages or warnings ;-)

Actually, in this case it is not so easy to produce an error message because the
patterns are translated away with translations and the resulting lambda's are
perfectly legal.

Tobias