[isabelle] Re-interpretation of locales does not generate abbreviations



I encountered the following odd behaviour: 
When interpreting a locale with a prefix, the expected abbreviations are
only generated if the locale has not been interpreted before with the
same parameters. 

This feature is quite confusing, as it makes modular design more
difficult: If you need an instance of a locale for your theory, you must
make sure that none of the theories you are importing has already
instantiated this locale, and otherwise use the other theory's
instantiation.

Is there any workaround, or plans to change this behaviour? [Or good
reasons to keep it as is?]

Example:

locale foo begin
  definition "bar \<equiv> True"
end

interpretation p1!: foo by unfold_locales
interpretation p2!: foo by unfold_locales

term p1.bar
term p2.bar (* Does not exist! *)


Regards
  Peter





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.