src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
changeset 62925 f1bdf10f95d8
parent 62601 a937889f0086
child 62969 9f394a16c557
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Apr 09 14:11:31 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Apr 09 14:17:50 2016 +0200
@@ -178,7 +178,7 @@
   [cvc4N, z3N, spassN, eN, vampireN, veritN, e_sineN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
-  |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))
+  |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))
   |> implode_param
 
 fun set_default_raw_param param thy =