[isabelle-dev] Structures [Strange interaction of locales and constant definitions]

[Clemens Ballarin]

Quoting Lars Noschinski <noschinl at in.tum.de>:

> BTW: Do you agree with me that M shouldn't be declared as structure?

I guess, you suggest that the annotation can be removed because only  
the first annotation has an effect.  This is a matter of taste, and I  
would prefer to keep them for reasons of symmetry.  Also, it makes  
refactoring easier.  That is, when restructuring the declarations, one  
does not spend time on inserting and deleting them along the way.

In an earlier implementation structures were indexed by numbers and  
the number for the first occurrence could be omitted.  After this was  
changed to structure names, I have kept all structure annotations for  
the above reasons.

Clemens