diff -r a085a1a89388 -r d892f6d66402 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Pure/Tools/build.ML	Wed Nov 11 21:00:14 2020 +0100
@@ -89,9 +89,9 @@
     (fn [args_yxml] =>
         let
           val (symbol_codes, (command_timings, (verbose, (browser_info,
-            (document_files, (graph_file, (parent_name, (chapter, (session_name, (master_dir,
+            (documents, (parent_name, (chapter, (session_name, (master_dir,
             (theories, (session_positions, (session_directories, (doc_names, (global_theories,
-            (loaded_theories, bibtex_entries)))))))))))))))) =
+            (loaded_theories, bibtex_entries))))))))))))))) =
             YXML.parse_body args_yxml |>
               let
                 open XML.Decode;
@@ -99,12 +99,12 @@
                 val path = Path.explode o string;
               in
                 pair (list (pair string int)) (pair (list properties) (pair bool (pair path
-                  (pair (list (pair path path)) (pair path (pair string (pair string (pair string
+                  (pair (list string) (pair string (pair string (pair string
                     (pair path
                       (pair (((list (pair Options.decode (list (pair string position))))))
                         (pair (list (pair string properties))
                           (pair (list (pair string string)) (pair (list string)
-                            (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))
+                            (pair (list (pair string string)) (pair (list string) (list string)))))))))))))))
               end;
 
           val symbols = HTML.make_symbols symbol_codes;
@@ -124,11 +124,7 @@
                   symbols
                   (Options.default_bool "browser_info")
                   browser_info
-                  (Options.default_string "document")
-                  (Options.default_string "document_output")
-                  (Present.document_variants (Options.default ()))
-                  document_files
-                  graph_file
+                  documents
                   parent_name
                   (chapter, session_name)
                   verbose;