src/Pure/System/session.ML

   val id: unit -> string list
   val name: unit -> string
   val welcome: unit -> string
   val finish: unit -> unit
   val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
-    string -> string -> string * Present.dump_mode -> string -> bool -> unit
+    string -> string -> bool * string -> string -> bool -> unit
   val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
   val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
     string -> bool -> string list -> string -> string -> bool * string ->
     string -> int -> bool -> bool -> int -> int -> int -> int -> unit
 end;

     doc_variants (path ()) name doc_dump (get_rpath rpath) verbose
     (map Thy_Info.get_theory (Thy_Info.get_names ())));
 
 local
 
-fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty);
-
 fun read_variants strs =
   rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
   |> filter_out (fn (_, s) => s = "-");
 
 in
 
 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
-    name dump rpath level timing verbose max_threads trace_threads
+    name doc_dump rpath level timing verbose max_threads trace_threads
     parallel_proofs parallel_proofs_threshold =
   ((fn () =>
     let
       val _ =
         Output.physical_stderr
           "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
       val _ =
         init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
-          (doc_dump dump) rpath verbose;
+          doc_dump rpath verbose;
       val res1 = (use |> with_timing item timing |> Exn.capture) root;
       val res2 = Exn.capture finish ();
     in ignore (Par_Exn.release_all [res1, res2]) end)
     |> Unsynchronized.setmp Proofterm.proofs level
     |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())