Email Gateway (Sep 21 2023 at 00:30): Email Gateway (Sep 21 2023 at 00:30):From: Fabian Huch <huch@in.tum.de>
When retrieving local propositions inside a proof and applying standard
operations on them (e.g., Thm.unconstrainT), I get the following error
(Isabelle2023):
exception CONTEXT ("No content for theory certificate Scratch:11571",
[], [], ["True"], NONE) raised (line 561 of "thm.ML")
The problem is easy to reproduce, e.g. with the following code:
proof -
have True ..
ML_val ‹Proof_Context.facts_of @{context} |> Facts.props |> map
(Thm.unconstrainT o fst)›
This is probably due to compression of some certificates inside this
context (where full certificates are replaced by ids). Is there any way
to work around this?
Fabian
Last updated: Apr 29 2024 at 04:18 UTC