diff -r b73678836f8e -r 6fb85346cb79 src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Wed May 09 20:45:57 2018 +0200
@@ -8,10 +8,7 @@
 sig
   val max_threads: unit -> int
   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
@@ -42,9 +39,6 @@
 
 fun max_threads () = ! max_threads_state;
 fun max_threads_update m = max_threads_state := max_threads_result m;
-fun enabled () = max_threads () > 1;
-
-val relevant = (fn [] => false | [_] => false | _ => enabled ());
 
 end;
 
@@ -53,9 +47,6 @@
 
 val parallel_proofs = ref 1;
 
-fun parallel_proofs_enabled n =
-  enabled () andalso ! parallel_proofs >= n;
-
 
 (* synchronous wait *)