--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Oct 29 18:23:29 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Oct 29 16:07:41 2020 +0100
@@ -57,13 +57,15 @@
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 =