--- a/src/HOL/Tools/Function/fun.ML	Sat Nov 30 13:40:57 2024 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Sat Nov 30 13:41:38 2024 +0100
@@ -66,8 +66,7 @@
         val n = arity_of fname
         val (argTs, rT) = chop n (binder_types fT)
           |> apsnd (fn Ts => Ts ---> body_type fT)
-
-        val qs = map Free (Name.invent_global "a" n ~~ argTs)
+        val qs = map Free (Name.invent_names_global "a" argTs)
       in
         HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
           Const (\<^const_name>\<open>undefined\<close>, rT))