[isabelle-dev] Shadowing of theorem names in locales

[Makarius]

On Thu, 11 Oct 2012, Johannes Hölzl wrote:

> HOL-Probability (in Isabelle/bb5db3d1d6dd) and
> Ordinary_Differential_Equations (in AFP/e9fa38f86b76) work now with this
> patch.
>
> A surprising change is found in Markov_Models:
>
>  We get an error when an assumption has the same name as a fact in the
>  locale:
>
>    locale loc
>    begin
>      lemma X: "True" ..
>
>      lemma assumes X: "X" shows "True"
>                    ^- raises "Duplicate fact declaration "local.X" vs. "local.X""
>
> Is this easily avoidable? I think this might confuse people and add a 
> maintenance burden when one adds a fact to a locale with a popular name.

It is a consequence of handling the local fact name space in a fully 
authentic way.  In the conversions I had done earlier, there were a few 
situations with duplicate assumptions of a long statement, so I just 
renamed them apart.


 	Makarius