unused (see 564012e31db1);
authorwenzelm
Mon, 28 Sep 2020 17:43:31 +0200
changeset 72321 09d1d7332185
parent 72320 c695d0b89586
child 72322 9bb16dcb9ed8
unused (see 564012e31db1);
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;