src/Pure/Thy/present.ML
changeset 72321 09d1d7332185
parent 72310 a756e464e9e3
child 72375 e48d93811ed7
--- 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;