# HG changeset patch
# User blanchet
# Date 1337589571 -7200
# Node ID 4073e51293cfff5edf0bb0ab1a2d3eaf5461c0f8
# Parent  e6b51fab96f796331a70c05adb526dfe95cf9af0
tuning

diff -r e6b51fab96f7 -r 4073e51293cf src/HOL/Tools/Sledgehammer/async_manager.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Mon May 21 10:39:31 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Mon May 21 10:39:31 2012 +0200
@@ -121,7 +121,7 @@
   |> AList.group (op =)
   |> List.app (fn ((tool, work), workers) =>
                   tool ^ ": " ^
-                  implode_message (workers |> sort string_ord, work)
+                  implode_message (workers |> sort_distinct string_ord, work)
                   |> break_into_chunks
                   |> List.app Output.urgent_message)