diff -r f76a5849b570 -r 08574da77b4a src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Tools/Code/code_preproc.ML	Fri Nov 29 17:40:15 2024 +0100
@@ -202,7 +202,7 @@
     val t = Thm.term_of ct;
     val vs_original =
       build (fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t);
-    val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original);
+    val vs_normalized = Name.invent_types_global (map snd vs_original);
     val normalize =
       map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
     val normalization =