src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 56081 72fad75baf7e
parent 55475 b8ebbcc5e49a
child 56084 75c154e9f650
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Mar 13 13:18:13 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Mar 13 13:18:13 2014 +0100
     1.3 @@ -184,7 +184,7 @@
     1.4        Metis_Method (SOME full_typesN, NONE),
     1.5        Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
     1.6        Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]) @
     1.7 -  (if smt_proofs then [SMT_Method] else [])
     1.8 +  (if smt_proofs then [SMT2_Method] else [])
     1.9  
    1.10  fun extract_proof_method ({type_enc, lam_trans, ...} : params)
    1.11        (Metis_Method (type_enc', lam_trans')) =
    1.12 @@ -195,7 +195,7 @@
    1.13          (if is_none lam_trans' andalso is_none lam_trans then []
    1.14           else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])])
    1.15      in (metisN, override_params) end
    1.16 -  | extract_proof_method _ SMT_Method = (smtN, [])
    1.17 +  | extract_proof_method _ SMT2_Method = (smtN, [])
    1.18  
    1.19  (* based on "Mirabelle.can_apply" and generalized *)
    1.20  fun timed_apply timeout tac state i =
    1.21 @@ -279,7 +279,8 @@
    1.22      val (remote_provers, local_provers) =
    1.23        proof_method_names @
    1.24        sort_strings (supported_atps thy) @
    1.25 -      sort_strings (SMT_Solver.available_solvers_of ctxt)
    1.26 +      sort_strings (SMT_Solver.available_solvers_of ctxt) @
    1.27 +      sort_strings (SMT2_Solver.available_solvers_of ctxt)
    1.28        |> List.partition (String.isPrefix remote_prefix)
    1.29    in
    1.30      Output.urgent_message ("Supported provers: " ^