--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Aug 04 13:24:54 2024 +0200
@@ -2271,7 +2271,7 @@
Formula ((tcon_clause_prefix ^ name, ""), Axiom,
mk_ahorn (maps (class_atoms type_enc) prems)
(class_atom type_enc (cl, T))
- |> bound_tvars type_enc true (snd (dest_Type T)),
+ |> bound_tvars type_enc true (dest_Type_args T),
NONE, isabelle_info generate_isabelle_info inductiveN helper_rank)
fun line_of_conjecture ctxt mono type_enc ({name, role, iformula, atomic_types, ...} : ifact) =