permissive treatment of citations before the theory header: avoid too many changes in AFP;
--- a/src/Pure/Thy/bibtex.ML Mon Jan 16 20:08:15 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML Mon Jan 16 20:40:42 2023 +0100
@@ -57,7 +57,9 @@
map (fn (name, pos) => (pos, Markup.citation name)) citations);
val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt);
- val bibtex_entries = Resources.theory_bibtex_entries thy_name;
+ val bibtex_entries =
+ if thy_name = Context.PureN then []
+ else Resources.theory_bibtex_entries thy_name;
val _ =
if null bibtex_entries andalso thy_name <> Context.PureN then ()
else