Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] File antiquotation broken after Theory.join_th...

view this post on Zulip Email Gateway (Jul 15 2020 at 14:34):

From: Norbert Schirmer via Cl-isabelle-users <>

After a “Theory.join_theory” a file antiquotation reports an error “no such file” for which it is perfectly happy before the join theory.
Note that the markup displayed in Isabelle/Jedit still appears as expected, only decorated with the error twigglies.

This can be demonstrated by HOl-ex.Join_Theory.thy

view this post on Zulip Email Gateway (Jul 16 2020 at 21:07):

From: Makarius <>
The problem is that Theory.join_theory performs a regular theory merge, which
historically appeared only in theory header position. Thus a few data slots
are reset to an empty value, notably the master directory of the theory: this
makes the @{file} antiquotation fail.

For now you can use the following change on Isabelle2020:

But this is not the last word: some more data slots need to be treated
similarly. I will probably also change the Theory_Data API to discontinue the
"extend" operation and its implicit impact on the "merge" operation. In those
rare cases where non-standard extend/merge is required, it can be done via
Theory.at_begin (e.g. see


Last updated: Dec 05 2021 at 22:18 UTC