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