[isabelle-dev] Problems with more rigorous check of simplifier context

[Florian Haftmann]

I stumbled over a problem with
http://isabelle.in.tum.de/repos/isabelle/rev/9ec2d47de6a7 and static
code conversions.

In static code conversions, it happens routinely that the cterm to which
the conversion is applied to stems from a different (but subsequent)
theory than the theory from the context of its construction.  See the
attached theory for a minimal example which actually only invokes pre-
and postprocessor.

This breaks in #9ec2d47de6a7 with »rewrite_cterm: bad background theory«.

Maybe this problem has nothing to do with the simplifier itself, but
rather how theories are handled in ML blocks.  E.g. in the attached
example the conversion succeeds if applied within the *same* ML block,
but always breaks in a further ML block, though the theory context there
is, according to my understanding, a subcontext of the first ML block,
and this is confirmed by the assertion in the attached example.

I'm confused.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Static_Closure.thy
Type: application/x-extension-thy
Size: 522 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130720/9e575343/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130720/9e575343/attachment.asc>