src/Pure/ProofGeneral/preferences.ML

   let
     fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
     fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
   in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
 
+val parallel_proof_pref =
+  let
+    fun get () = PgipTypes.bool_to_pgstring (! Goal.parallel_proofs >= 1);
+    fun set s = Goal.parallel_proofs := (if PgipTypes.read_pgipbool s then 1 else 0);
+  in mkpref get set PgipTypes.Pgipbool "parallel-proofs" "Check proofs in parallel" end;
+
 val thm_depsN = "thm_deps";
 val thm_deps_pref =
   let
     fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN);
     fun set s =

     "Skip over proofs (interactive-only)",
   proof_pref,
   nat_pref Multithreading.max_threads
     "max-threads"
     "Maximum number of threads",
-  bool_pref Goal.parallel_proofs
-    "parallel-proofs"
-    "Check proofs in parallel"];
+  parallel_proof_pref];
 
 val pure_preferences =
  [(category_display, display_preferences),
   (category_advanced_display, advanced_display_preferences),
   (category_tracing, tracing_preferences),