# HG changeset patch
# User wenzelm
# Date 1514578663 -3600
# Node ID 48ca44fdc038a571f89c0a6756d49a832f0b5e67
# Parent  e255c76db0525f1ee783bde108b51edd855fc2fb
no check for bibtex entries from other sessions;

diff -r e255c76db052 -r 48ca44fdc038 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Dec 29 19:53:43 2017 +0100
+++ b/src/Pure/Thy/present.ML	Fri Dec 29 21:17:43 2017 +0100
@@ -312,13 +312,15 @@
       val html_source = HTML.theory symbols name parent_specs (mk_text ());
       val _ = init_theory_info name (make_theory_info ("", html_source));
 
-      val _ =
+      val bibtex_entries' =
         if is_session_theory thy then
           (add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name));
-           add_tex_index (update_time, Latex.theory_entry name))
-        else ();
+           add_tex_index (update_time, Latex.theory_entry name);
+           bibtex_entries)
+        else [];
     in
-      Browser_Info.put {chapter = chapter, name = session_name, bibtex_entries = bibtex_entries} thy
+      thy
+      |> Browser_Info.put {chapter = chapter, name = session_name, bibtex_entries = bibtex_entries'}
     end);
 
 end;