tuning
authorblanchet
Mon May 21 10:39:31 2012 +0200 (2012-05-21)
changeset 479454073e51293cf
parent 47944 e6b51fab96f7
child 47946 33afcfad3f8d
tuning
src/HOL/Tools/Sledgehammer/async_manager.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Mon May 21 10:39:31 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Mon May 21 10:39:31 2012 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4    |> AList.group (op =)
     1.5    |> List.app (fn ((tool, work), workers) =>
     1.6                    tool ^ ": " ^
     1.7 -                  implode_message (workers |> sort string_ord, work)
     1.8 +                  implode_message (workers |> sort_distinct string_ord, work)
     1.9                    |> break_into_chunks
    1.10                    |> List.app Output.urgent_message)
    1.11