tuned;

--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sat Nov 30 13:27:15 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sat Nov 30 13:40:57 2024 +0100
@@ -1315,8 +1315,8 @@
         else (c, d) :: (add_association a b r);
 
     fun new_TVar known_TVars =
-      Name.invent_list (map (fst o fst o dest_TVar) known_TVars) "x" 1
-      |> (fn [s] => TVar ((s, 0), []));
+      let val [a] = Name.invent_list (map (fst o fst o dest_TVar) known_TVars) Name.aT 1
+      in TVar ((a, 0), []) end
 
     fun instantiate_type inferred_types =
       Term.typ_subst_TVars (map (apfst (fst o dest_TVar)) inferred_types);

--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Sat Nov 30 13:27:15 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Sat Nov 30 13:40:57 2024 +0100
@@ -50,7 +50,7 @@
 fun check_size_type thy T_name size_name =
   let
     val n = Sign.arity_number thy T_name;
-    val As = map (fn s => TFree (s, \<^sort>\<open>type\<close>)) (Name.invent_global_types n);
+    val As = map (fn a => TFree (a, \<^sort>\<open>type\<close>)) (Name.invent_global_types n);
     val T = Type (T_name, As);
     val size_T = map mk_to_natT As ---> mk_to_natT T;
     val size_const = Const (size_name, size_T);

--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sat Nov 30 13:27:15 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sat Nov 30 13:40:57 2024 +0100
@@ -642,8 +642,7 @@
     fun inter_sort m =
       map (fn xs => nth xs m) raw_vss
       |> foldr1 (Sorts.inter_sort (Sign.classes_of thy));
-    val sorts = map inter_sort ms;
-    val vs = Name.invent_types_global sorts;
+    val vs = Name.invent_types_global (map inter_sort ms);
 
     fun norm_constr (raw_vs, (c, T)) =
       (c, map_atyps