On 7 Jun 2009, at 11:39, Roger Bishop Jones wrote:

I have now a fairly complicated theory hierarchy
and its easy to mistakenly use a name which has already
been used somewhere.

I did this today and the resulting failure mode
seemed rather odd, so I wondered whether this is
how it is supposed to be or a sign of something amiss.

I defined the constant "Set" in a theory of miscellanea
("rbjmisc") high up in my hierarchy, forgetting that
this constant had already been used elsewhere.
It turned out that the previous use was in one of the
few theories which did not name rbjmisc as a parent,
so the second definition of Set went through OK, in
theory "nfu_f".

Then another theory is built which has both nfu_f and
rbjmisc as parents, causing a clash of names.
No complaint when the two parents are first nominated. ...


The name clash should definitely cause an error. Perhaps you are catching the error somehow?

Regards,

Rob.



_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to