src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

             end
         val s12 = merge s1 s2
         val t1 = try_metis s1 s0 ()
         val t2 = try_metis s2 (SOME s1) ()
         val timeout =
-          t1 + t2 |> Time.toReal |> curry Real.* merge_timeout_slack
+          Time.+ (t1, t2) |> Time.toReal |> curry Real.* merge_timeout_slack
                   |> Time.fromReal
       in
         (TimeLimit.timeLimit timeout (try_metis s12 s0) ();
          SOME (front @ (the_list s0 @ s12 :: tail)))
         handle _ => NONE