diff -r 3e17f343deb5 -r c5d0f19ef7cb src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Thu Jul 26 14:24:27 2012 +0200
+++ b/src/Pure/System/build.ML	Thu Jul 26 14:29:54 2012 +0200
@@ -65,7 +65,7 @@
         (Options.bool options "document_graph")
         (space_explode ":" (Options.string options "document_variants"))
         parent_base_name base_name
-        (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
+        (Options.string options "document_dump", Options.string options "document_dump_mode")
         "" verbose;
     val _ = Session.with_timing name timing (List.app use_theories) theories;
     val _ = Session.finish ();