--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Oct 29 18:23:29 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Oct 29 16:07:41 2020 +0100
@@ -360,7 +360,7 @@
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
val preferred_methss =
(Metis_Method (NONE, NONE),
- bunches_of_proof_methods try0 smt_proofs needs_full_types
+ bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types
(if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN))
in
(used_facts, preferred_methss,