[isabelle-dev] Shadowing of theorem names in locales

[Makarius]

On Mon, 8 Oct 2012, Clemens Ballarin wrote:

> On the other hand, if theory information is not stored in the internal 
> name, theory merges can result in invalid locales (that is, locales that 
> cannot even be activated, leaving alone interpreted).

This is a general principle: global merges of theory date are always 
endangered, there is no guarantee that the result works.  So it is the 
normal order of things, but with the slight modification that for locales 
the crash is deferred to the point where the user attempts to use the 
result.

Testing well-formedness of merged locales at the theory header is probably 
a bit too expensive.  We also have a general tendency towards deferred 
declarations (e.g. in bundles) so non-strict theory content will occur 
more often in the future.


 	Makarius