# HG changeset patch
# User blanchet
# Date 1306068702 -7200
# Node ID ddff373cf3adf935a73a9bfa8a4aba782e917fc6
# Parent  cb28abfde010bffa9fa0676acd8d0bb0c7d5708a
added message when Waldmeister isn't run

diff -r cb28abfde010 -r ddff373cf3ad src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun May 22 14:51:42 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun May 22 14:51:42 2011 +0200
@@ -168,8 +168,9 @@
 
 val auto_max_relevant_divisor = 2 (* FUDGE *)
 
-fun run_sledgehammer (params as {debug, blocking, provers, relevance_thresholds,
-                                 max_relevant, slicing, timeout, ...})
+fun run_sledgehammer (params as {debug, verbose, blocking, provers,
+                                 relevance_thresholds, max_relevant, slicing,
+                                 timeout, ...})
         auto i (relevance_override as {only, ...}) minimize_command state =
   if null provers then
     error "No prover is set."
@@ -244,8 +245,16 @@
                        ())
         end
       fun launch_atps label is_good_prop atps accum =
-        if null atps orelse not (is_good_prop concl_t) then
+        if null atps then
           accum
+        else if not (is_good_prop concl_t) then
+          (if verbose orelse length atps = length provers then
+             "Goal outside the scope of " ^
+             space_implode " " (serial_commas "and" (map quote atps)) ^ "."
+             |> Output.urgent_message
+           else
+             ();
+           accum)
         else
           launch_provers state
               (get_facts label is_good_prop atp_relevance_fudge o K atps)