1.1 --- a/src/HOL/Tools/try0.ML	Mon Nov 04 17:25:36 2013 +0100
     1.2 +++ b/src/HOL/Tools/try0.ML	Mon Nov 04 18:08:47 2013 +0100
     1.3 @@ -108,12 +108,16 @@
     1.4     ("presburger", ((false, true), no_attrs))]
     1.5  val do_methods = map do_named_method named_methods
     1.6  
     1.7 -fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
     1.8 +fun time_string ms = string_of_int ms ^ " ms"
     1.9 +fun tool_time_string (s, ms) = s ^ ": " ^ time_string ms
    1.10  
    1.11  fun do_try0 mode timeout_opt quad st =
    1.12    let
    1.13      val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #>
    1.14        Config.put Lin_Arith.verbose false)
    1.15 +    fun par_map f =
    1.16 +      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself snd)
    1.17 +      else Par_List.get_some f #> the_list
    1.18    in
    1.19      if mode = Normal then
    1.20        "Trying " ^ space_implode " " (Try.serial_commas "and"
    1.21 @@ -121,8 +125,7 @@
    1.22        |> Output.urgent_message
    1.23      else
    1.24        ();
    1.25 -    case do_methods |> Par_List.map (fn f => f mode timeout_opt quad st)
    1.26 -                    |> map_filter I |> sort (int_ord o pairself snd) of
    1.27 +    case par_map (fn f => f mode timeout_opt quad st) do_methods of
    1.28        [] =>
    1.29        (if mode = Normal then Output.urgent_message "No proof found." else ();
    1.30         (false, (noneN, st)))
    1.31 @@ -140,7 +143,9 @@
    1.32            Active.sendback_markup [Markup.padding_command]
    1.33                ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
    1.34                  else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
    1.35 -          "\n(" ^ space_implode "; " (map time_string xs) ^ ")."
    1.36 +          (case xs of
    1.37 +            [(_, ms)] => " (" ^ time_string ms ^ ")."
    1.38 +          | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").")
    1.39        in
    1.40          (true, (s, st |> (if mode = Auto_Try then
    1.41                              Proof.goal_message