# HG changeset patch
# User wenzelm
# Date 1733059450 -3600
# Node ID e8b388c2b49047b11f301db44f0dc0918a03c423
# Parent  1bfad73ab115f6bfcba22a392a4034f4350559c8
tuned;

diff -r 1bfad73ab115 -r e8b388c2b490 src/HOL/Hoare/hoare_tac.ML
--- 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);
diff -r 1bfad73ab115 -r e8b388c2b490 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- 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". *)
diff -r 1bfad73ab115 -r e8b388c2b490 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- 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);