src/Pure/System/build.ML

         (Options.bool options "browser_info") browser_info
         (Options.string options "document")
         (Options.bool options "document_graph")
         (space_explode ":" (Options.string options "document_variants"))
         parent_name name
-        (Options.string options "document_dump", Options.string options "document_dump_mode")
+        (Options.string options "document_dump",
+          Present.dump_mode (Options.string options "document_dump_mode"))
         "" verbose;
     val _ = Session.with_timing name timing (List.app use_theories) theories;
     val _ = Session.finish ();
     val _ = if do_output then () else quit ();
   in () end