src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
changeset 55297 1dfcd49f5dcb
parent 55288 1a4358d14ce2
child 55308 dc68f6fb88d2
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 19:32:02 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 19:32:02 2014 +0100
     1.3 @@ -212,7 +212,7 @@
     1.4      do_slice timeout 1 NONE Time.zeroTime
     1.5    end
     1.6  
     1.7 -fun run_smt_solver mode name (params as {debug, verbose, smt, preplay_timeout, ...})
     1.8 +fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
     1.9      minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
    1.10    let
    1.11      val thy = Proof.theory_of state
    1.12 @@ -234,7 +234,7 @@
    1.13          NONE =>
    1.14          (Lazy.lazy (fn () =>
    1.15             play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
    1.16 -             SMT_Method (bunch_of_proof_methods (smt <> SOME false) false liftingN)),
    1.17 +             SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
    1.18           fn preplay =>
    1.19              let
    1.20                val one_line_params =