[isabelle-dev] Shadowing of theorem names in locales

[Clemens Ballarin]

 On 21 March, 2014 17:26 CET, Makarius <makarius at sketis.net> wrote: 
 
> On Tue, 11 Feb 2014, Clemens Ballarin wrote:
> 
> > For the processing of locale expression, facts are not really required. 
> > Having all information related to syntax should be sufficient.  I cannot 
> > tell, though, whether facts may contain syntax in disguise of certain 
> > attributes.
> 
> In principle there could be arbitrary declarations disguised as 
> declaration attributes of facts, but the general sanity assumption is that 
> this is not done.  The separate concept of syntax_declaration was 
> introduced for that, when we sorted this out several years ago.

To be more precise about what I had said above: I actually believe that syntax is only required when parsing a locale (i.e. reading it for the first time).  When activating it later, everything should be set, and the syntax should no longer matter.

Clemens