--- a/src/HOL/TPTP/atp_problem_import.ML Fri Oct 15 19:25:31 2021 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Fri Oct 15 20:54:13 2021 +0200
@@ -130,7 +130,8 @@
(** Sledgehammer and Isabelle (combination of provers) **)
fun can_tac ctxt tactic conj =
- can (Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj)) (fn [] => tactic ctxt)
+ \<^can>\<open>Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj)
+ (fn {context = goal_ctxt, prems = []} => tactic goal_ctxt)\<close>
fun SOLVE_TIMEOUT seconds name tac st =
let