src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML

           if timeout <= min_timeout then
             NONE
           else
             let val y = f timeout x in
               (case get_time y of
-                SOME time => next_timeout := time
+                SOME time => next_timeout := time_min (time, !next_timeout)
               | _ => ());
               SOME y
             end
         end
     in
-      map_filter I (Par_List.map apply_f xs)
+      chop_groups (Multithreading.max_threads ()) xs
+      |> map (map_filter I o Par_List.map apply_f)
+      |> flat
     end
 
 fun enrich_context_with_local_facts proof ctxt =
   let
     val thy = Proof_Context.theory_of ctxt