[isabelle] defining a constant with a long-identifier name



I want to (programmatically) define constants that live within
different sub-spaces of the same theory, and so might have the same
name.  I know this is possible, because it is what the record package
achieves if you write

----------------------------------------------------------------------
theory foo
  imports Main

begin

record rec1 =
  fld1 :: nat
  fld2 :: bool

record rec2 =
  fld1 :: bool

end;
----------------------------------------------------------------------

There are two "fld1" constants after this is executed: foo.rec1.fld1
and foo.rec2.fld1.

However, the function Theory.add_consts_i takes a "bstring", and does
not allow the declaration of qualified names.

So, how does the record package do it?  (And, just in case the answers
are not the same, how should I do it myself?)

Michael.





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