Stream: Isabelle/ML

Topic: "No content for theory certificate" for local propositions

view this post on Zulip Fabian Huch (Sep 20 2023 at 15:33):

(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?

view this post on Zulip Fabian Huch (Sep 20 2023 at 15:57):

So Thm.transfer' does solve the issue (thanks @Simon Roßkopf ), but I still have no clue why this should be necessary.

Last updated: May 04 2024 at 08:17 UTC