# 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)