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
Static_Closure.thy
Description: application/extension-thy
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
