# HG changeset patch
# User blanchet
# Date 1283460616 -7200
# Node ID a74bd9bfa8801b78865473e2f39f88cbe39103d1
# Parent  ceee95f4182338b1552c0a9b5ea389efc9ad144e
show the number of facts for each prover in "verbose" mode

diff -r ceee95f41823 -r a74bd9bfa880 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 02 22:49:56 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 02 22:50:16 2010 +0200
@@ -366,14 +366,23 @@
 
 fun get_prover_fun thy name = prover_fun name (get_prover thy name)
 
-fun run_prover ctxt (params as {blocking, timeout, expect, ...}) i n
-               relevance_override minimize_command
-               (problem as {goal, ...}) (prover, atp_name) =
+fun run_prover ctxt (params as {blocking, verbose, max_relevant, timeout,
+                                expect, ...})
+               i n relevance_override minimize_command
+               (problem as {goal, axioms, ...})
+               (prover as {default_max_relevant, ...}, atp_name) =
   let
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, timeout)
+    val max_relevant = the_default default_max_relevant max_relevant
+    val num_axioms = Int.min (length axioms, max_relevant)
     val desc =
-      "ATP " ^ quote atp_name ^ " for subgoal " ^ string_of_int i ^ ":" ^
+      "ATP " ^ quote atp_name ^
+      (if verbose then
+         " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms
+       else
+         "") ^
+      " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
       (if blocking then
          ""
        else
@@ -431,11 +440,6 @@
               {ctxt = ctxt, goal = goal, subgoal = i,
                axioms = map (prepare_axiom ctxt) axioms}
             val num_axioms = length axioms
-            val _ = if verbose then
-                      priority ("Selected " ^ string_of_int num_axioms ^
-                                " fact" ^ plural_s num_axioms ^ ".")
-                    else
-                      ()
             val _ =
               (if blocking then Par_List.map else map)
                   (run_prover ctxt params i n relevance_override