# HG changeset patch
# User blanchet
# Date 1358109759 -3600
# Node ID 48836c35d636542f4519f056f74ca8fa0691caf0
# Parent  e12ebcb859a7d9c333f541d93590855910cd43a4
have Mirabelle produce more output

diff -r e12ebcb859a7 -r 48836c35d636 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun Jan 13 21:42:38 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun Jan 13 21:42:39 2013 +0100
@@ -477,12 +477,20 @@
           |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
                  (the_default default_max_facts max_facts)
                  Sledgehammer_Fact.no_fact_override hyp_ts concl_t
+          |> map (apfst (apfst (fn name => name ())))
+          |> tap (fn facts =>
+                     (if null facts then
+                        "Found no relevant facts."
+                      else
+                        "Including " ^ string_of_int (length facts) ^
+                        " relevant fact(s):\n" ^
+                        (facts |> map (fst o fst) |> space_implode " ") ^ ".")
+                     |> Output.urgent_message)
         val prover = get_prover ctxt prover_name params goal facts
         val problem =
           {state = st', goal = goal, subgoal = i,
            subgoal_count = Sledgehammer_Util.subgoal_count st,
-           facts = facts |> map (apfst (apfst (fn name => name ())))
-                         |> map Sledgehammer_Provers.Untranslated_Fact}
+           facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
       in prover params (K (K (K ""))) problem end)) ()
       handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
            | Fail "inappropriate" => failed ATP_Proof.Inappropriate