(This is a cross-post from the mailing list)
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?
So Thm.transfer'
does solve the issue (thanks @Simon Roßkopf ), but I still have no clue why this should be necessary.
Last updated: Dec 07 2024 at 16:22 UTC