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

[Tjark Weber]

On Wed, 2012-04-04 at 11:19 +0200, Tobias Nipkow wrote:
> No, a feature. Patterns may not contain repeated variables.

But this is not being enforced; instead, repeated variables are silently
renamed.

Adhering to the principle of least astonishment, I suspect an error
message (or at least a warning) would be more helpful.

Best regards,
Tjark