permissive treatment of citations before the theory header: avoid too many changes in AFP;
authorwenzelm
Mon, 16 Jan 2023 20:40:42 +0100
changeset 76995 467f45e79ff9
parent 76994 7c23db6b857b
child 76996 6d847e27cafc
permissive treatment of citations before the theory header: avoid too many changes in AFP;
src/Pure/Thy/bibtex.ML
--- 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