# HG changeset patch
# User wenzelm
# Date 1732970498 -3600
# Node ID c1aa8a61ee654ab11263fd811ecf6ac9c00f1cd3
# Parent  8cbc8bc6f3821b14a325cee1cf2bb559d945d66d
tuned: more direct use of Name.context operations;

diff -r 8cbc8bc6f382 -r c1aa8a61ee65 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Sat Nov 30 13:40:57 2024 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Sat Nov 30 13:41:38 2024 +0100
@@ -66,8 +66,7 @@
         val n = arity_of fname
         val (argTs, rT) = chop n (binder_types fT)
           |> apsnd (fn Ts => Ts ---> body_type fT)
-
-        val qs = map Free (Name.invent_global "a" n ~~ argTs)
+        val qs = map Free (Name.invent_names_global "a" argTs)
       in
         HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
           Const (\<^const_name>\<open>undefined\<close>, rT))
diff -r 8cbc8bc6f382 -r c1aa8a61ee65 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Nov 30 13:40:57 2024 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Nov 30 13:41:38 2024 +0100
@@ -72,7 +72,7 @@
 
 fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
   let
-    val frees = map Free (Name.invent_names_global "a" (map (K \<^typ>\<open>narrowing_term\<close>) tys))
+    val frees = map (fn a => Free (a, \<^typ>\<open>narrowing_term\<close>)) (Name.invent_global "a" (length tys))
     val narrowing_term =
       \<^term>\<open>Quickcheck_Narrowing.Narrowing_constructor\<close> $ HOLogic.mk_number \<^typ>\<open>integer\<close> i $
         HOLogic.mk_list \<^typ>\<open>narrowing_term\<close> (rev frees)
diff -r 8cbc8bc6f382 -r c1aa8a61ee65 src/Pure/Build/export_theory.ML
--- a/src/Pure/Build/export_theory.ML	Sat Nov 30 13:40:57 2024 +0100
+++ b/src/Pure/Build/export_theory.ML	Sat Nov 30 13:41:38 2024 +0100
@@ -263,7 +263,7 @@
         val args' = args |> filter (is_free o #1);
         val typargs' = typargs |> filter (is_free o #1);
         val used_typargs = fold (Name.declare o #1) typargs' used;
-        val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
+        val sorts = Name.invent_types used_typargs extra_shyps;
       in ((sorts @ typargs', args', prop), proof) end;
 
     fun standard_prop_of thm =
diff -r 8cbc8bc6f382 -r c1aa8a61ee65 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Sat Nov 30 13:40:57 2024 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sat Nov 30 13:41:38 2024 +0100
@@ -211,9 +211,8 @@
   let
     fun rew_term Ts t =
       let
-        val frees =
-          map Free
-            (Name.invent (Name.build_context (Term.declare_free_names t)) "xa" (length Ts) ~~ Ts);
+        val names = Name.build_context (Term.declare_free_names t);
+        val frees = map Free (Name.invent_names names "xa" Ts);
         val t' = r (subst_bounds (frees, t));
         fun strip [] t = t
           | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
diff -r 8cbc8bc6f382 -r c1aa8a61ee65 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Nov 30 13:40:57 2024 +0100
+++ b/src/Pure/axclass.ML	Sat Nov 30 13:41:38 2024 +0100
@@ -280,12 +280,12 @@
     val binding =
       Binding.concealed (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
 
-    val args = Name.invent_types_global Ss;
+    val args = map TFree (Name.invent_types_global Ss);
     val missing_params =
       Sign.complete_sort thy [c]
       |> maps (these o Option.map #params o try (get_info thy))
       |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
-      |> (map o apsnd o map_atyps) (K (Type (t, map TFree args)));
+      |> (map o apsnd o map_atyps) (K (Type (t, args)));
   in
     thy
     |> Global_Theory.store_thm (binding, th)
diff -r 8cbc8bc6f382 -r c1aa8a61ee65 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sat Nov 30 13:40:57 2024 +0100
+++ b/src/Pure/logic.ML	Sat Nov 30 13:41:38 2024 +0100
@@ -335,7 +335,7 @@
 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
 
 fun mk_arities (t, Ss, S) =
-  let val T = Type (t, ListPair.map TFree (Name.invent_global_types (length Ss), Ss))
+  let val T = Type (t, map TFree (Name.invent_types_global Ss))
   in map (fn c => mk_of_class (T, c)) S end;
 
 fun mk_arity (t, Ss, c) = the_single (mk_arities (t, Ss, [c]));
diff -r 8cbc8bc6f382 -r c1aa8a61ee65 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Nov 30 13:40:57 2024 +0100
+++ b/src/Pure/variable.ML	Sat Nov 30 13:41:38 2024 +0100
@@ -594,7 +594,7 @@
 
 fun invent_types Ss ctxt =
   let
-    val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss;
+    val tfrees = Name.invent_types (names_of ctxt) Ss;
     val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   in (tfrees, ctxt') end;