src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 55297 1dfcd49f5dcb
parent 55288 1a4358d14ce2
child 55308 dc68f6fb88d2
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 19:32:02 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 19:32:02 2014 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4       isar_proofs : bool option,
     1.5       compress_isar : real,
     1.6       try0_isar : bool,
     1.7 -     smt : bool option,
     1.8 +     smt_proofs : bool option,
     1.9       slice : bool,
    1.10       minimize : bool option,
    1.11       timeout : Time.time,
    1.12 @@ -147,7 +147,7 @@
    1.13     isar_proofs : bool option,
    1.14     compress_isar : real,
    1.15     try0_isar : bool,
    1.16 -   smt : bool option,
    1.17 +   smt_proofs : bool option,
    1.18     slice : bool,
    1.19     minimize : bool option,
    1.20     timeout : Time.time,
    1.21 @@ -183,7 +183,7 @@
    1.22    | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
    1.23    | _ => "Try this")
    1.24  
    1.25 -fun bunch_of_proof_methods smt needs_full_types desperate_lam_trans =
    1.26 +fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
    1.27    [Metis_Method (SOME full_type_enc, NONE)] @
    1.28    (if needs_full_types then
    1.29       [Metis_Method (SOME full_type_enc, NONE),
    1.30 @@ -193,7 +193,7 @@
    1.31       [Metis_Method (NONE, NONE),
    1.32        Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) @
    1.33    [Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] @
    1.34 -  (if smt then [SMT_Method] else [])
    1.35 +  (if smt_proofs then [SMT_Method] else [])
    1.36  
    1.37  fun extract_proof_method ({type_enc, lam_trans, ...} : params)
    1.38        (Metis_Method (type_enc', lam_trans')) =