tuning
authorblanchet
Mon, 21 May 2012 10:39:31 +0200
changeset 47945 4073e51293cf
parent 47944 e6b51fab96f7
child 47946 33afcfad3f8d
tuning
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)