src/Pure/System/session.ML

   rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
   |> filter_out (fn (_, s) => s = "-");
 
 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
     name doc_dump rpath level timing verbose max_threads trace_threads
-    parallel_proofs parallel_proofs_threshold =
+    parallel_proofs parallel_subproofs_saturation =
   ((fn () =>
     let
       val _ =
         Output.physical_stderr
           "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";

       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 ())
     |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
-    |> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold
+    |> Unsynchronized.setmp Goal.parallel_subproofs_saturation parallel_subproofs_saturation
     |> Unsynchronized.setmp Multithreading.trace trace_threads
     |> Unsynchronized.setmp Multithreading.max_threads
       (if Multithreading.available then max_threads
        else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
   handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);