# HG changeset patch
# User blanchet
# Date 1288251411 -7200
# Node ID 7883fefd6a7b11bf4700853c986a0a96df9054f2
# Parent  9f001f7e6c0c90c5e467df2f95a5fa2f665d3b4b
clear identification;
thread "Auto S/H" (vs. manual S/H) setting through SMT

diff -r 9f001f7e6c0c -r 7883fefd6a7b src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Oct 28 09:29:57 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Oct 28 09:36:51 2010 +0200
@@ -266,7 +266,7 @@
      "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
 
 fun proof_banner auto =
-  if auto then "Sledgehammer found a proof" else "Try this command"
+  if auto then "Auto Sledgehammer found a proof" else "Try this command"
 
 (* generic TPTP-based ATPs *)
 
@@ -399,7 +399,7 @@
     val (conjecture_shape, fact_names) =
       repair_conjecture_shape_and_fact_names output conjecture_shape fact_names
     val important_message =
-      if random () <= important_message_keep_factor then
+      if not auto andalso random () <= important_message_keep_factor then
         extract_important_message output
       else
         ""
@@ -432,7 +432,7 @@
   | failure_from_smt_failure SMT_Solver.Out_Of_Memory = OutOfResources
   | failure_from_smt_failure _ = UnknownError
 
-fun run_smt_solver remote ({timeout, ...} : params) minimize_command
+fun run_smt_solver auto remote ({timeout, ...} : params) minimize_command
                    ({state, subgoal, subgoal_count, facts, ...}
                     : prover_problem) =
   let
@@ -443,7 +443,7 @@
     val message =
       case outcome of
         NONE =>
-        try_command_line (proof_banner false)
+        try_command_line (proof_banner auto)
                          (apply_on_subgoal subgoal subgoal_count ^
                           command_call smtN (map fst used_facts)) ^
         minimize_line minimize_command (map fst used_facts)
@@ -458,8 +458,10 @@
   end
 
 fun get_prover thy auto name =
-  if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix name)
-  else run_atp auto name (get_atp thy name)
+  if is_smt_prover name then
+    run_smt_solver auto (String.isPrefix remote_prefix name)
+  else
+    run_atp auto name (get_atp thy name)
 
 fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
                auto minimize_command