--- 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;