--- a/src/HOL/Import/import_rule.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/HOL/Import/import_rule.ML Sun Dec 01 14:01:47 2024 +0100
@@ -335,7 +335,7 @@
val thm = Drule.export_without_context_open thm
val tvs = Term.add_tvars (Thm.prop_of thm) []
val tns = map (fn (_, _) => "'") tvs
- val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt))
+ val nms = Name.variants (Variable.names_of ctxt) tns
val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
val thm' = Thm.instantiate (TVars.make (tvs ~~ map (Thm.ctyp_of ctxt) vs), Vars.empty) thm
in
--- a/src/HOL/Nominal/nominal_primrec.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Sun Dec 01 14:01:47 2024 +0100
@@ -34,7 +34,7 @@
let
val (vs, Ts) = split_list (strip_qnt_vars \<^const_name>\<open>Pure.all\<close> t);
val body = strip_qnt_body \<^const_name>\<open>Pure.all\<close> t;
- val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
+ val vs' = vs |> Name.variants (Name.make_context (fold_aterms
(fn Free (v, _) => insert (op =) v | _ => I) body []))
in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Sun Dec 01 14:01:47 2024 +0100
@@ -260,7 +260,7 @@
let
val T = dest_Const_type c;
val Ts = binder_types T;
- val (names, _) = fold_map Name.variant (make_tnames Ts) used;
+ val names = Name.variants used (make_tnames Ts);
val ty = body_type T;
val ty_theta = Type.raw_match (ty, colty) Vartab.empty
handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);
@@ -304,10 +304,9 @@
then
let
val Ts = map fastype_of ps;
- val (xs, _) =
- fold_map Name.variant
- (replicate (length ps) "x")
- (fold Term.declare_free_names gvars used');
+ val xs =
+ Name.variants (fold Term.declare_free_names gvars used')
+ (replicate (length ps) "x");
in
[((prfx, gvars @ map Free (xs ~~ Ts)),
(Const (\<^const_name>\<open>undefined\<close>, res_ty), ~1))]
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Sun Dec 01 14:01:47 2024 +0100
@@ -38,7 +38,7 @@
let
val (vs, Ts) = split_list (strip_qnt_vars \<^const_name>\<open>Pure.all\<close> spec);
val body = strip_qnt_body \<^const_name>\<open>Pure.all\<close> spec;
- val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
+ val vs' = vs |> Name.variants (Name.make_context (fold_aterms
(fn Free (v, _) => insert (op =) v | _ => I) body []));
val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body;
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eqn)
--- a/src/Pure/Isar/code.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/Pure/Isar/code.ML Sun Dec 01 14:01:47 2024 +0100
@@ -1465,8 +1465,7 @@
fun case_cong thy case_const (num_args, (pos, _)) =
let
- val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context;
- val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt;
+ val x :: y :: zs = Name.variants Name.context ("A" :: "A'" :: replicate (num_args - 1) "");
val (ws, vs) = chop pos zs;
val T = devarify (const_typ thy case_const);
val Ts = binder_types T;
--- a/src/Pure/name.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/Pure/name.ML Sun Dec 01 14:01:47 2024 +0100
@@ -41,6 +41,7 @@
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 variants: context -> string list -> string list
val variant_list: string list -> string list -> string list
val enforce_case: bool -> string -> string
val desymbolize: bool option -> string -> string
@@ -177,7 +178,8 @@
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);
+fun variants ctxt xs = #1 (fold_map variant xs ctxt);
+val variant_list = variants o make_context;
(* names conforming to typical requirements of identifiers in the world outside *)
--- a/src/Pure/type.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/Pure/type.ML Sun Dec 01 14:01:47 2024 +0100
@@ -346,7 +346,7 @@
build (t |> (Term.fold_types o Term.fold_atyps)
(fn TFree v => if TFrees.defined fixed v then I else insert (op =) v | _ => I));
val used = Name.build_context (t |> Term.declare_tvar_names (K true));
- val ys = #1 (fold_map Name.variant (map #1 xs) used);
+ val ys = Name.variants used (map #1 xs);
in map2 (fn (a, S) => fn b => ((a, S), ((b, 0), S))) xs ys end;
fun varify_global fixed t =
--- a/src/Pure/variable.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/Pure/variable.ML Sun Dec 01 14:01:47 2024 +0100
@@ -327,7 +327,7 @@
| bounds =>
let
val names = Term.declare_term_names t (names_of ctxt);
- val xs = rev (#1 (fold_map Name.variant (rev (map #2 bounds)) names));
+ val xs = rev (Name.variants names (rev (map #2 bounds)));
fun substs (((b, T), _), x') =
let fun subst U = (Free (b, U), Syntax_Trans.mark_bound_abs (x', U))
in [subst T, subst (Type_Annotation.ignore_type T)] end;
--- a/src/Tools/Code/code_printer.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/Tools/Code/code_printer.ML Sun Dec 01 14:01:47 2024 +0100
@@ -188,7 +188,7 @@
val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
val x = singleton (Name.variant_list (map_filter I fished1)) "x";
val fished2 = map_index (fillup_param x) fished1;
- val (fished3, _) = fold_map Name.variant fished2 Name.context;
+ val fished3 = Name.variants Name.context fished2;
val vars' = intro_vars fished3 vars;
in map (lookup_var vars') fished3 end;
--- a/src/Tools/IsaPlanner/isand.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/Tools/IsaPlanner/isand.ML Sun Dec 01 14:01:47 2024 +0100
@@ -57,7 +57,7 @@
val names =
Variable.names_of ctxt
|> fold (fn t => Term.declare_free_names t #> Term.declare_var_names (K true) t) ts;
- in fst (fold_map Name.variant xs names) end;
+ in Name.variants names xs end;
(* fix parameters of a subgoal "i", as free variables, and create an
exporting function that will use the result of this proved goal to