1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 05 12:40:48 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 05 12:40:48 2011 +0200
     1.3 @@ -461,10 +461,10 @@
     1.4                     * 0.001) |> seconds
     1.5                  val _ =
     1.6                    if debug then
     1.7 -                    quote name ^ " slice " ^ string_of_int (slice + 1) ^
     1.8 -                    " of " ^ string_of_int num_actual_slices ^ " with " ^
     1.9 -                    string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
    1.10 -                    " for " ^ string_from_time slice_timeout ^ "..."
    1.11 +                    quote name ^ " slice #" ^ string_of_int (slice + 1) ^
    1.12 +                    " with " ^ string_of_int num_facts ^ " fact" ^
    1.13 +                    plural_s num_facts ^ " for " ^
    1.14 +                    string_from_time slice_timeout ^ "..."
    1.15                      |> Output.urgent_message
    1.16                    else
    1.17                      ()