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
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.
Similarly, in theory "nfu_f":
:) print_theory "nfu_f";
=== The theory nfu_f ===
--- Constants ---
$nf SETnf SETnf BOOL
SETnf
mk_const("Set", SETnf BOOL®)®
SETnf BOOL
Ur SETnf 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?
Roger Jones
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
