clarified modules;

--- a/src/Pure/Concurrent/multithreading.ML	Mon Apr 23 21:57:15 2018 +0100
+++ b/src/Pure/Concurrent/multithreading.ML	Tue Apr 24 11:03:51 2018 +0200
@@ -10,6 +10,8 @@
   val max_threads_update: int -> unit
   val enabled: unit -> bool
   val relevant: 'a list -> bool
+  val parallel_proofs: int ref
+  val parallel_proofs_enabled: int -> bool
   val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
   val trace: int ref
   val tracing: int -> (unit -> string) -> unit
@@ -47,6 +49,14 @@
 end;
 
 
+(* parallel_proofs *)
+
+val parallel_proofs = ref 1;
+
+fun parallel_proofs_enabled n =
+  enabled () andalso ! parallel_proofs >= n;
+
+
 (* synchronous wait *)
 
 fun sync_wait time cond lock =

--- a/src/Pure/System/isabelle_process.ML	Mon Apr 23 21:57:15 2018 +0100
+++ b/src/Pure/System/isabelle_process.ML	Tue Apr 24 11:03:51 2018 +0200
@@ -218,14 +218,14 @@
   Future.ML_statistics := Options.default_bool "ML_statistics";
   Multithreading.trace := Options.default_int "threads_trace";
   Multithreading.max_threads_update (Options.default_int "threads");
-  Goal.parallel_proofs := Options.default_int "parallel_proofs";
+  Multithreading.parallel_proofs := Options.default_int "parallel_proofs";
   let val proofs = Options.default_int "record_proofs"
   in if proofs < 0 then () else Proofterm.proofs := proofs end;
   Printer.show_markup_default := false);
 
 fun init_options_interactive () =
  (init_options ();
-  Goal.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0);
+  Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0);
   Printer.show_markup_default := true);
 
 end;

--- a/src/Pure/goal.ML	Mon Apr 23 21:57:15 2018 +0100
+++ b/src/Pure/goal.ML	Tue Apr 24 11:03:51 2018 +0200
@@ -7,7 +7,6 @@
 signature BASIC_GOAL =
 sig
   val quick_and_dirty: bool Config.T
-  val parallel_proofs: int Unsynchronized.ref
   val SELECT_GOAL: tactic -> int -> tactic
   val PREFER_GOAL: tactic -> int -> tactic
   val CONJUNCTS: tactic -> int -> tactic
@@ -112,10 +111,8 @@
     else skip
   end;
 
-val parallel_proofs = Unsynchronized.ref 1;
-
 fun future_enabled n =
-  Multithreading.enabled () andalso ! parallel_proofs >= n andalso
+  Multithreading.parallel_proofs_enabled n andalso
   is_some (Future.worker_task ());
 
 fun future_enabled_timing t =