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