diff -r 8cbc8bc6f382 -r c1aa8a61ee65 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sat Nov 30 13:40:57 2024 +0100
+++ b/src/Pure/logic.ML	Sat Nov 30 13:41:38 2024 +0100
@@ -335,7 +335,7 @@
 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
 
 fun mk_arities (t, Ss, S) =
-  let val T = Type (t, ListPair.map TFree (Name.invent_global_types (length Ss), Ss))
+  let val T = Type (t, map TFree (Name.invent_types_global Ss))
   in map (fn c => mk_of_class (T, c)) S end;
 
 fun mk_arity (t, Ss, c) = the_single (mk_arities (t, Ss, [c]));