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