src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
changeset 56081 72fad75baf7e
parent 55452 29ec8680e61f
child 56303 4cc3f4db3447
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 13 13:18:13 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 13 13:18:13 2014 +0100
     1.3 @@ -234,7 +234,7 @@
     1.4          NONE =>
     1.5          (Lazy.lazy (fn () =>
     1.6             play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
     1.7 -             SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
     1.8 +             SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
     1.9           fn preplay =>
    1.10              let
    1.11                val one_line_params =