tuned behavior of 'smt' option

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -16,11 +16,11 @@
   val trace : bool Config.T
 
   type isar_params =
-    bool * (string option * string option) * Time.time * real * bool * bool * bool
+    bool * (string option * string option) * Time.time * real * bool * bool
     * (term, string) atp_step list * thm
 
-  val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int ->
-    one_line_params -> string
+  val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
+    int -> one_line_params -> string
 end;
 
 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
@@ -108,7 +108,7 @@
     end
 
 type isar_params =
-  bool * (string option * string option) * Time.time * real * bool * bool * bool
+  bool * (string option * string option) * Time.time * real * bool * bool
   * (term, string) atp_step list * thm
 
 val arith_methods =
@@ -126,18 +126,18 @@
 val skolem_methods =
   [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
 
-fun isar_proof_text ctxt debug isar_proofs isar_params
+fun isar_proof_text ctxt debug isar_proofs smt isar_params
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
     fun isar_proof_of () =
       let
-        val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, smt, minimize,
+        val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
           atp_proof, goal) = try isar_params ()
 
         val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
 
         fun massage_meths (meths as meth :: _) =
-          if not try0_isar then [meth] else if smt then SMT_Method :: meths else meths
+          if not try0_isar then [meth] else if smt = SOME true then SMT_Method :: meths else meths
 
         val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
         val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
@@ -355,18 +355,18 @@
           if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
   in one_line_proof ^ isar_proof end
 
-fun isar_proof_would_be_a_good_idea (meth, play) =
+fun isar_proof_would_be_a_good_idea smt (meth, play) =
   (case play of
-    Played _ => meth = SMT_Method
+    Played _ => meth = SMT_Method andalso smt <> SOME true
   | Play_Timed_Out _ => true
   | Play_Failed => true
   | Not_Played => false)
 
-fun proof_text ctxt debug isar_proofs isar_params num_chained
+fun proof_text ctxt debug isar_proofs smt isar_params num_chained
     (one_line_params as (preplay, _, _, _, _, _)) =
   (if isar_proofs = SOME true orelse
-      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
-     isar_proof_text ctxt debug isar_proofs isar_params
+      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt preplay) then
+     isar_proof_text ctxt debug isar_proofs smt isar_params
    else
      one_line_proof_text num_chained) one_line_params
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -372,7 +372,7 @@
                       |> factify_atp_proof fact_names hyp_ts concl_t
                   in
                     (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress_isar,
-                     try0_isar, smt = SOME true, minimize |> the_default true, atp_proof, goal)
+                     try0_isar, minimize |> the_default true, atp_proof, goal)
                   end
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
@@ -380,7 +380,7 @@
                    subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
-                proof_text ctxt debug isar_proofs isar_params num_chained one_line_params
+                proof_text ctxt debug isar_proofs smt isar_params num_chained one_line_params
               end,
            (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
            (if important_message <> "" then