# HG changeset patch
# User blanchet
# Date 1304592048 -7200
# Node ID d4f5fec71ded7ce358d1e363a7e9b27cf902b94a
# Parent  ffd1ae4ff5c6ce9dc46202776932f16533554c78
no lies in debug output (e.g. "slice 2 of 1")

diff -r ffd1ae4ff5c6 -r d4f5fec71ded src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 05 12:40:48 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 05 12:40:48 2011 +0200
@@ -461,10 +461,10 @@
                    * 0.001) |> seconds
                 val _ =
                   if debug then
-                    quote name ^ " slice " ^ string_of_int (slice + 1) ^
-                    " of " ^ string_of_int num_actual_slices ^ " with " ^
-                    string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
-                    " for " ^ string_from_time slice_timeout ^ "..."
+                    quote name ^ " slice #" ^ string_of_int (slice + 1) ^
+                    " with " ^ string_of_int num_facts ^ " fact" ^
+                    plural_s num_facts ^ " for " ^
+                    string_from_time slice_timeout ^ "..."
                     |> Output.urgent_message
                   else
                     ()