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 @@ -126,7 +126,7 @@
     1.4  val skolem_methods =
     1.5    [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
     1.6  
     1.7 -fun isar_proof_text ctxt debug isar_proofs smt isar_params
     1.8 +fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
     1.9      (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
    1.10    let
    1.11      fun isar_proof_of () =
    1.12 @@ -137,7 +137,9 @@
    1.13          val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
    1.14  
    1.15          fun massage_meths (meths as meth :: _) =
    1.16 -          if not try0_isar then [meth] else if smt = SOME true then SMT_Method :: meths else meths
    1.17 +          if not try0_isar then [meth]
    1.18 +          else if smt_proofs = SOME true then SMT_Method :: meths
    1.19 +          else meths
    1.20  
    1.21          val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
    1.22          val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
    1.23 @@ -355,18 +357,18 @@
    1.24            if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
    1.25    in one_line_proof ^ isar_proof end
    1.26  
    1.27 -fun isar_proof_would_be_a_good_idea smt (meth, play) =
    1.28 +fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
    1.29    (case play of
    1.30 -    Played _ => meth = SMT_Method andalso smt <> SOME true
    1.31 +    Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
    1.32    | Play_Timed_Out _ => true
    1.33    | Play_Failed => true
    1.34    | Not_Played => false)
    1.35  
    1.36 -fun proof_text ctxt debug isar_proofs smt isar_params num_chained
    1.37 +fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
    1.38      (one_line_params as (preplay, _, _, _, _, _)) =
    1.39    (if isar_proofs = SOME true orelse
    1.40 -      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt preplay) then
    1.41 -     isar_proof_text ctxt debug isar_proofs smt isar_params
    1.42 +      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
    1.43 +     isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
    1.44     else
    1.45       one_line_proof_text num_chained) one_line_params
    1.46