# HG changeset patch
# User wenzelm
# Date 1732996919 -3600
# Node ID 1b33a7a3c80c6afcc731f5d053158fec4db4e481
# Parent  31b05aef022d3dc2e9d3153d235764ff66d9fd57
tuned signature: more operations;

diff -r 31b05aef022d -r 1b33a7a3c80c src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Sat Nov 30 19:21:38 2024 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Sat Nov 30 21:01:59 2024 +0100
@@ -478,10 +478,7 @@
                 map (pair "x") (drop j (take i (binder_types (fastype_of t)))), [])
               else chop i zs;
             val u = fold_rev Term.abs ys (strip_abs_body t);
-            val xs' = map Free
-              ((fold_map Name.variant (map fst xs)
-                  (Term.declare_term_names u used) |> fst) ~~
-               map snd xs);
+            val xs' = map Free (Name.variant_names (Term.declare_term_names u used) xs);
             val (xs1, xs2) = chop j xs'
           in (xs', list_comb (subst_bounds (rev xs1, u), xs2)) end;
         fun is_dependent i t =
diff -r 31b05aef022d -r 1b33a7a3c80c src/Pure/name.ML
--- a/src/Pure/name.ML	Sat Nov 30 19:21:38 2024 +0100
+++ b/src/Pure/name.ML	Sat Nov 30 21:01:59 2024 +0100
@@ -39,6 +39,8 @@
   val invent_list: string list -> string -> int -> string list
   val variant: string -> context -> string * context
   val variant_bound: string -> context -> string * context
+  val variant_names: context -> (string * 'a) list -> (string * 'a) list
+  val variant_names_build: (context -> context) -> (string * 'a) list -> (string * 'a) list
   val variant_list: string list -> string list -> string list
   val enforce_case: bool -> string -> string
   val desymbolize: bool option -> string -> string
@@ -172,6 +174,9 @@
 
 fun variant_bound name = variant (if is_bound name then "u" else name);
 
+fun variant_names ctxt xs = #1 (fold_map (variant o fst) xs ctxt) ~~ map snd xs;
+fun variant_names_build f xs = variant_names (build_context f) xs;
+
 fun variant_list used names = #1 (make_context used |> fold_map variant names);
 
 
diff -r 31b05aef022d -r 1b33a7a3c80c src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Nov 30 19:21:38 2024 +0100
+++ b/src/Pure/term.ML	Sat Nov 30 21:01:59 2024 +0100
@@ -603,8 +603,7 @@
   declare_tfree_names tm;
 
 fun variant_frees t frees =
-  #1 (fold_map Name.variant (map fst frees) (Name.build_context (declare_term_names t))) ~~
-    map #2 frees;
+  Name.variant_names_build (declare_term_names t) frees;
 
 
 (* sorts *)
diff -r 31b05aef022d -r 1b33a7a3c80c src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Nov 30 19:21:38 2024 +0100
+++ b/src/Pure/variable.ML	Sat Nov 30 21:01:59 2024 +0100
@@ -278,10 +278,7 @@
 (* renaming term/type frees *)
 
 fun variant_frees ctxt ts frees =
-  let
-    val names = names_of (fold declare_names ts ctxt);
-    val xs = fst (fold_map Name.variant (map #1 frees) names);
-  in xs ~~ map snd frees end;
+  Name.variant_names (names_of (fold declare_names ts ctxt)) frees;