[isabelle] referring to constants that have just been defined



If I have just defined a constant (using add_constdefs_i, say), and
want to construct a new term including that new constant term, how
should I generate that term?

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?

Is there a function that will give me the name of the current theory,
so that I can construct the fully-qualified name myself?  

Or is there some other way again?

Thanks,
Michael.






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