Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
no lies in debug output (e.g. "slice 2 of 1")
authorblanchet
Thu, 05 May 2011 12:40:48 +0200
changeset 42699 d4f5fec71ded
parent 42698 ffd1ae4ff5c6
child 42700 f4d17cc370f9
no lies in debug output (e.g. "slice 2 of 1")
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML file | annotate | diff | comparison | revisions 
--- 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
                     ()
isabelle