src/Pure/name.ML

--- 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 *)