Re: [isabelle] referring to constants that have just been defined



On Mon, 27 Mar 2006, Michael Norrish wrote:

> It seems that using 
> 
>   Sign.intern_const
> 
> will give me the correct qualified name for the constant (I do know
> its name after all), but I'm worried about the situation when multiple
> constants from different theories have the same name.  What will
> intern_const do then?

You are right in being worried. Above `intern' only worked by chance, 
because a recent declaration is likely to be preferred by name space 
lookup.

Name spaces provide 3 key operations:

  full -- produce fully qualified name according to the current naming policy

  intern -- internalize an external name (partically qualified) according 
    to the current name space (for reading etc.)

  extern -- reverse of intern (for printing etc.)

You want to perform the `full' operation here, ie. mimic what 
add_constdefs_i did internally.  Do this via Sign.full_name, which uses 
the official naming convention of the theory context.  Do not refer to 
theory_name etc. directly.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.