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           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?

Roger Jones



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

Reply via email to