--- a/src/HOL/Hoare/hoare_tac.ML Sun Dec 01 14:01:47 2024 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML Sun Dec 01 14:24:10 2024 +0100
@@ -87,7 +87,7 @@
fun Mset ctxt prop =
let
- val [(Mset, _), (P, _)] = Variable.variant_names ctxt [("Mset", ()), ("P", ())];
+ val [Mset, P] = Name.variants (Variable.names_of ctxt) ["Mset", "P"];
val vars = get_vars prop;
val varsT = fastype_of (mk_bodyC vars);
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Dec 01 14:01:47 2024 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Dec 01 14:24:10 2024 +0100
@@ -278,7 +278,7 @@
ATP-generated Skolem function names, since these end with a digit and
"variant_frees" appends letters. *)
fun desymbolize_and_fresh_up ctxt s =
- fst (singleton (Variable.variant_names ctxt) (Name.desymbolize (SOME false) s, ()))
+ #1 (Name.variant (Name.desymbolize (SOME false) s) (Variable.names_of ctxt))
(* Higher-order translation. Variables are typed (although we don't use that information). Lambdas
are typed. The code is similar to "term_of_atp_fo". *)
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sun Dec 01 14:01:47 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sun Dec 01 14:24:10 2024 +0100
@@ -262,7 +262,7 @@
|> mk_TFrees' (map Type.sort_of_atyp As0);
val fpT = Type (fpT_name, As);
- val (var_name, ()) = singleton (Variable.variant_names ctxt) ("x", ());
+ val var_name = #1 (Name.variant "x" (Variable.names_of ctxt));
val var = Free (var_name, fpT);
val goal = mk_Trueprop_eq (expand_to_ctr_term ctxt fpT var, var);