[isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name

[Brian Huffman]

Hello everyone,

Isabelle prints out warning messages whenever anyone declares a
duplicate simp rule, intro rule, etc. It would be nice if Isabelle
would print a similar warning whenever a definition reuses a name that
is already in scope in the current context. For example, if a theory
defines a class like this...

class complete_boolean_algebra = distributive_complete_lattice + boolean_algebra

...and a class called "complete_boolean_algebra" is already in scope,
then a warning message ought to be printed.

Such a warning message would be useful for constant names, lemma
names, etc. as well.

- Brian