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