diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Function/function_elims.ML
--- a/src/HOL/Tools/Function/function_elims.ML	Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Function/function_elims.ML	Sun Aug 04 13:24:54 2024 +0200
@@ -109,7 +109,7 @@
 
         val (rhs_var, arg_vars, prop) = mk_funeq arity (fastype_of f) ([], f);
         val args = HOLogic.mk_tuple arg_vars;
-        val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
+        val domT = hd (dest_Type_args (snd (dest_Free R)));
 
         val P = Thm.cterm_of ctxt (variant_free prop ("P", \<^typ>\<open>bool\<close>));
         val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx + 1) args;