--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 16:53:58 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 17:13:31 2014 +0100
@@ -132,7 +132,7 @@
fun run_atp mode name
(params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
- try0_isar, slice, minimize, timeout, preplay_timeout, ...})
+ try0_isar, smt, slice, minimize, timeout, preplay_timeout, ...})
minimize_command
({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
@@ -347,7 +347,7 @@
val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
val meths =
- bunch_of_proof_methods needs_full_types
+ bunch_of_proof_methods (smt <> SOME false) needs_full_types
(if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
in
(used_facts,
@@ -372,7 +372,7 @@
|> factify_atp_proof fact_names hyp_ts concl_t
in
(verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress_isar,
- try0_isar, minimize |> the_default true, atp_proof, goal)
+ try0_isar, smt = SOME true, minimize |> the_default true, atp_proof, goal)
end
val one_line_params =
(preplay, proof_banner mode name, used_facts,