diff -r ac7af931189f -r f5896dea6fce src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Jan 20 16:30:09 2023 +0100
+++ b/src/Pure/PIDE/resources.ML	Fri Jan 20 19:52:52 2023 +0100
@@ -10,7 +10,6 @@
   val init_session:
     {session_positions: (string * Properties.T) list,
      session_directories: (string * string) list,
-     bibtex_entries: (string * string list) list,
      command_timings: Properties.T list,
      load_commands: (string * Position.T) list,
      scala_functions: (string * ((bool * bool) * Position.T)) list,
@@ -30,7 +29,6 @@
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val thy_path: Path.T -> Path.T
   val theory_qualifier: string -> string
-  val theory_bibtex_entries: string -> string list
   val find_theory_file: string -> Path.T option
   val import_name: string -> Path.T -> string ->
     {node_name: Path.T, master_dir: Path.T, theory_name: string}
@@ -105,7 +103,6 @@
 val empty_session_base =
   ({session_positions = []: (string * entry) list,
     session_directories = Symtab.empty: Path.T list Symtab.table,
-    bibtex_entries = Symtab.empty: string list Symtab.table,
     timings = empty_timings,
     load_commands = []: (string * Position.T) list,
     scala_functions = Symtab.empty: ((bool * bool) * Position.T) Symtab.table},
@@ -116,7 +113,7 @@
   Synchronized.var "Sessions.base" empty_session_base;
 
 fun init_session
-    {session_positions, session_directories, bibtex_entries, command_timings, load_commands,
+    {session_positions, session_directories, command_timings, load_commands,
       scala_functions, global_theories, loaded_theories} =
   Synchronized.change global_session_base
     (fn _ =>
@@ -124,7 +121,6 @@
         session_directories =
           Symtab.build (session_directories |> fold_rev (fn (dir, name) =>
             Symtab.cons_list (name, Path.explode dir))),
-        bibtex_entries = Symtab.make bibtex_entries,
         timings = make_timings command_timings,
         load_commands = load_commands,
         scala_functions = Symtab.make scala_functions},
@@ -133,22 +129,21 @@
 
 fun init_session_yxml yxml =
   let
-    val (session_positions, (session_directories, (bibtex_entries, (command_timings,
-        (load_commands, (scala_functions, (global_theories, loaded_theories))))))) =
+    val (session_positions, (session_directories, (command_timings,
+        (load_commands, (scala_functions, (global_theories, loaded_theories)))))) =
       YXML.parse_body_bytes yxml |>
         let open XML.Decode in
           (pair (list (pair string properties))
             (pair (list (pair string string))
-              (pair (list (pair string (list string))) (pair (list properties)
+              (pair (list properties)
                 (pair (list (pair string properties))
                   (pair (list (pair string (pair (pair bool bool) properties)))
-                    (pair (list (pair string string)) (list string))))))))
+                    (pair (list (pair string string)) (list string)))))))
         end;
   in
     init_session
       {session_positions = session_positions,
        session_directories = session_directories,
-       bibtex_entries = bibtex_entries,
        command_timings = command_timings,
        load_commands = (map o apsnd) Position.of_properties load_commands,
        scala_functions = (map o apsnd o apsnd) Position.of_properties scala_functions,
@@ -268,9 +263,6 @@
   if literal_theory theory then theory
   else Long_Name.qualify qualifier theory;
 
-fun theory_bibtex_entries theory =
-  Symtab.lookup_list (get_session_base1 #bibtex_entries) (theory_qualifier theory);
-
 fun find_theory_file thy_name =
   let
     val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name));