diff -r 1c451bbb3ad7 -r 3e060b1c844b src/HOL/Tools/Sledgehammer/async_manager.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Fri May 27 10:30:08 2011 +0200
@@ -32,7 +32,7 @@
 val implode_desc = op ^ o apfst quote
 
 fun implode_message (workers, work) =
-  space_implode " " (ATP_Proof.serial_commas "and" (map quote workers)) ^ work
+  space_implode " " (Try.serial_commas "and" (map quote workers)) ^ work
 
 
 (* data structures over threads *)