# HG changeset patch
# User wenzelm
# Date 1673898042 -3600
# Node ID 467f45e79ff9ec7d254a6743d5e40a871a0e7095
# Parent  7c23db6b857b2549888948c3daf9fce0ad5c3f78
permissive treatment of citations before the theory header: avoid too many changes in AFP;

diff -r 7c23db6b857b -r 467f45e79ff9 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