src/HOL/Tools/Sledgehammer/async_manager_legacy.ML

--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Fri Sep 20 14:28:13 2024 +0200
@@ -19,7 +19,7 @@
 struct
 
 fun implode_message (workers, work) =
-  space_implode " " (Try.serial_commas "and" workers) ^ work
+  implode_space (Try.serial_commas "and" workers) ^ work
 
 structure Thread_Heap = Heap
 (