--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Oct 25 21:17:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Oct 26 09:40:20 2010 +0200
@@ -157,7 +157,7 @@
prover :: avoid_too_many_local_threads thy n provers
end
-val num_processors = try Thread.numProcessors #> the_default 1
+fun num_processors () = try Thread.numProcessors () |> the_default 1
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
timeout, it makes sense to put SPASS first. *)