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

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?



Proofpower mailing list

Reply via email to