diff -r f76a5849b570 -r 08574da77b4a src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Fri Nov 29 11:26:17 2024 +0100
+++ b/src/HOL/Typerep.thy	Fri Nov 29 17:40:15 2024 +0100
@@ -48,7 +48,7 @@
 fun add_typerep tyco thy =
   let
     val sorts = replicate (Sign.arity_number thy tyco) \<^sort>\<open>typerep\<close>;
-    val vs = Name.invent_names Name.context "'a" sorts;
+    val vs = Name.invent_types_global sorts;
     val ty = Type (tyco, map TFree vs);
     val lhs = \<^Const>\<open>typerep ty\<close> $ Free ("T", Term.itselfT ty);
     val rhs = \<^Const>\<open>Typerep\<close> $ HOLogic.mk_literal tyco