changeset 72518 | 4be6ae020fc4 |
parent 72513 | 75f5c63f6cfa |
child 72582 | b69a3a7655f2 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 29 18:23:29 2020 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 29 16:07:41 2020 +0100 @@ -160,7 +160,7 @@ fun massage_methods (meths as meth :: _) = if not try0 then [meth] - else if smt_proofs then SMT_Method :: meths + else if smt_proofs then SMT_Method SMT_Default :: meths else meths val (params, _, concl_t) = strip_subgoal goal subgoal ctxt