diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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) =