# HG changeset patch
# User blanchet
# Date 1271683295 -7200
# Node ID 109dce8410d5fd5edd496eb91fbd6b4da6e6e090
# Parent  217ca1273786c862b749f15a40c3f738c3c7dc19
cosmetics

diff -r 217ca1273786 -r 109dce8410d5 src/HOL/Tools/ATP_Manager/atp_minimal.ML
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Apr 19 15:15:21 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Apr 19 15:21:35 2010 +0200
@@ -88,10 +88,10 @@
                       prover atp_name i state name_thms_pairs =
   let
     val msecs = Time.toMilliseconds minimize_timeout
+    val n = length name_thms_pairs
     val _ =
-      priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
-        " theorems, ATP: " ^ atp_name ^
-        ", time limit: " ^ string_of_int msecs ^ " ms")
+      priority ("Sledgehammer minimizer: ATP " ^ quote atp_name ^
+                " with a time limit of " ^ string_of_int msecs ^ " ms.")
     val test_thms_fun =
       sledgehammer_test_theorems params prover minimize_timeout i state
     fun test_thms filtered thms =
@@ -104,8 +104,7 @@
   in
     (* try prove first to check result and get used theorems *)
     (case test_thms_fun NONE name_thms_pairs of
-      (Success, result as {internal_thm_names, filtered_clauses,
-                           ...}) =>
+      (Success, result as {internal_thm_names, filtered_clauses, ...}) =>
         let
           val used = internal_thm_names |> Vector.foldr (op ::) []
                                         |> sort_distinct string_ord
@@ -117,8 +116,9 @@
           val (min_thms, {conjecture_pos, proof, internal_thm_names, ...}) =
             linear_minimize (test_thms (SOME filtered_clauses)) to_use
                             ([], result)
+          val n = length min_thms
           val _ = priority (cat_lines
-            ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
+            ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
         in
           (SOME min_thms,
            proof_text isar_proof true modulus sorts atp_name