--- 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)