1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 19:32:02 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 19:32:02 2014 +0100
     1.3 @@ -16,11 +16,11 @@
     1.4    val trace : bool Config.T
     1.5  
     1.6    type isar_params =
     1.7 -    bool * (string option * string option) * Time.time * real * bool * bool * bool
     1.8 +    bool * (string option * string option) * Time.time * real * bool * bool
     1.9      * (term, string) atp_step list * thm
    1.10  
    1.11 -  val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int ->
    1.12 -    one_line_params -> string
    1.13 +  val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
    1.14 +    int -> one_line_params -> string
    1.15  end;
    1.16  
    1.17  structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
    1.18 @@ -108,7 +108,7 @@
    1.19      end
    1.20  
    1.21  type isar_params =
    1.22 -  bool * (string option * string option) * Time.time * real * bool * bool * bool
    1.23 +  bool * (string option * string option) * Time.time * real * bool * bool
    1.24    * (term, string) atp_step list * thm
    1.25  
    1.26  val arith_methods =
    1.27 @@ -126,18 +126,18 @@
    1.28  val skolem_methods =
    1.29    [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
    1.30  
    1.31 -fun isar_proof_text ctxt debug isar_proofs isar_params
    1.32 +fun isar_proof_text ctxt debug isar_proofs smt isar_params
    1.33      (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
    1.34    let
    1.35      fun isar_proof_of () =
    1.36        let
    1.37 -        val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, smt, minimize,
    1.38 +        val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
    1.39            atp_proof, goal) = try isar_params ()
    1.40  
    1.41          val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
    1.42  
    1.43          fun massage_meths (meths as meth :: _) =
    1.44 -          if not try0_isar then [meth] else if smt then SMT_Method :: meths else meths
    1.45 +          if not try0_isar then [meth] else if smt = SOME true then SMT_Method :: meths else meths
    1.46  
    1.47          val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
    1.48          val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
    1.49 @@ -355,18 +355,18 @@
    1.50            if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
    1.51    in one_line_proof ^ isar_proof end
    1.52  
    1.53 -fun isar_proof_would_be_a_good_idea (meth, play) =
    1.54 +fun isar_proof_would_be_a_good_idea smt (meth, play) =
    1.55    (case play of
    1.56 -    Played _ => meth = SMT_Method
    1.57 +    Played _ => meth = SMT_Method andalso smt <> SOME true
    1.58    | Play_Timed_Out _ => true
    1.59    | Play_Failed => true
    1.60    | Not_Played => false)
    1.61  
    1.62 -fun proof_text ctxt debug isar_proofs isar_params num_chained
    1.63 +fun proof_text ctxt debug isar_proofs smt isar_params num_chained
    1.64      (one_line_params as (preplay, _, _, _, _, _)) =
    1.65    (if isar_proofs = SOME true orelse
    1.66 -      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
    1.67 -     isar_proof_text ctxt debug isar_proofs isar_params
    1.68 +      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt preplay) then
    1.69 +     isar_proof_text ctxt debug isar_proofs smt isar_params
    1.70     else
    1.71       one_line_proof_text num_chained) one_line_params
    1.72