[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


record rec1 =
  fld1 :: nat
  fld2 :: bool

record rec2 =
  fld1 :: bool


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


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