# HG changeset patch
# User wenzelm
# Date 1601307811 -7200
# Node ID 09d1d73321855381a6b1f1d5db200f14ee3b67a8
# Parent  c695d0b8958685864bf37166736c1f648085a609
unused (see 564012e31db1);

diff -r c695d0b89586 -r 09d1d7332185 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Sep 28 16:43:49 2020 +0200
+++ b/src/Pure/Thy/present.ML	Mon Sep 28 17:43:31 2020 +0200
@@ -225,8 +225,8 @@
   write_tex (index_buffer tex_index) doc_indexN path;
 
 fun finish () =
-  with_session_info () (fn {name, chapter, info, info_path, document,
-    doc_output, doc_files, graph_file, documents, verbose, readme, ...} =>
+  with_session_info () (fn {name, chapter, info, info_path, doc_output, doc_files, graph_file,
+    documents, verbose, readme, ...} =>
   let
     val {theories, tex_index, html_index} = Synchronized.value browser_info;
     val thys = Symtab.dest theories;