Roger,
On 9 Jun 2009, at 07:23, Roger Bishop Jones wrote:
On Monday 08 June 2009 22:59:01 Rob Arthan wrote:
The name clash should definitely cause an error. Perhaps you are
catching the error somehow?
I don't think so.
Re-instating the error, I end up in a context in which
rbjmisc is an ancestor:
:) get_ancestors "-";
val it =
["pre_func", "catfun", "nfu_f", "cache'rbjhold", "\250", "dyadic",
"\175",
"analysis", "equiv_rel", "fincomb", "cache'maths_egs", "groups",
"group_egs", "bin_rel", "fun_rel", "seq", "fin_set", "topology",
"rbjmisc", "orders", "set_thms", "ordered_sets", "U_orders",
"one",
"combin", "sum", "min", "log", "init", "misc", "pair", "\238",
"list",
"char", "basic_hol", "sets", "hol", "tc", "wf_relp", "fixp",
"metapi"]
: string list
but in which "Set" is not a constant:
:) get_spec ¬Set®;
Exception Fail * ¬Set® is not a constant, or a constant applied to
some
arguments
That is only telling you that the parser doesn't think "Set" is the
name of a constant (which isn't a guaranteed test of const-ness: it
can happen even when the name is that of a constant in scope if you've
used undeclare_alias).
The theory listing corroborates this obliquely:
:) print_theory "rbjmisc";
=== The theory rbjmisc ===
--- Constants ---
CombC ('a – 'b – 'c) – 'b – 'a – 'c
PDisj 'a SET SET – BOOL
FunImage ('a – 'b) – 'a SET – 'b SET
Œmk_const("Set", ‰'a NESET – 'a SET®)®
'a NESET – 'a SET
NeSet 'a SET – 'a NESET
$Ÿ≈L 'a – 'a LIST – BOOL
Set is listed as a constant, but printed as if it were not in scope.
What do map dest_const(get_consts"tbjmisc") and map dest_const
(get_consts"nfu_f") come up with?
Similarly, in theory "nfu_f":
:) print_theory "nfu_f";
=== The theory nfu_f ===
--- Constants ---
$Ÿ≈nf SET≈nf – SET≈nf – BOOL
˚ SET≈nf
Œmk_const("Set", ‰SET≈nf – BOOL®)®
SET≈nf – BOOL
Ur SET≈nf – BOOL
So both definitions are out of scope.
Tracing back to the point at which the clash should have happened
there is no sign of this in the log.
val FuncCatCon_def = ... : THM
val it = () : unit
val it = () : unit
val it = () : unit
The first "unit" is "force_new_theory", the second is
`new_parent"nfu_f";'
and the clash should have been seen then.
Is this what would have happened if I had caught an exception?
No. if new_parent failed, then it shouldn't have made the theory a
parent. All I meant was that you might have failed to make the theory
a parent without noticing, but that doesn't seem to be the problem.
Is it possible to supply a version of your source (ideally cut down to
a minimum) that I can have a look at?
Regards,
Rob.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
