[isabelle] problem with local theories and the code generator



Hi,
I've experienced the following problem with ML-level of Isabelle (namely with local theories and the code generator):

My code is inside the command quotient_type and thus inside a local_theory context. In this context a new constant is defined (by Local_Theory.define) and it's called let's say "abs". Because I am inside a local_theory context, this constant is actually a fixed variable and not a real constant. So far so good. But now I want to call Code.add_datatype and thus say that "abs" is a code datatype constructor. I do it by the following command:
Local_Theory.declaration {syntax = false, pervasive = true}
 (K (Context.mapping (Code.add_datatype [(name, type)]) I))

But then the code generator complains that "abs" is not a constant.
How can I solve this situation? It seems to me that I need
either a) jump away from a local_theory context for a while and let "abs" get transformed to a real constant
or b) I need something like a "localized" code generator package.

Thanks for an answer.

Cheers,
Ondrej





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