src/HOL/Tools/Sledgehammer/async_manager_legacy.ML

--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -96,7 +96,7 @@
       let
         fun time_limit timeout_heap =
           (case try Thread_Heap.min timeout_heap of
-            NONE => Time.+ (Time.now (), max_wait_time)
+            NONE => Time.now () + max_wait_time
           | SOME (time, _) => time)
 
         (*action: find threads whose timeout is reached, and interrupt canceling threads*)