diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Sun Aug 04 17:39:47 2024 +0200
@@ -181,7 +181,7 @@
 
 fun varify_type ctxt T =
   Variable.polymorphic_types ctxt [Const (\<^const_name>\<open>undefined\<close>, T)]
-  |> snd |> the_single |> dest_Const |> snd
+  |> snd |> the_single |> dest_Const_type
 
 (* TODO: use "Term_Subst.instantiateT" instead? *)
 fun instantiate_type thy T1 T1' T2 =