diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Nov 30 22:33:21 2024 +0100
@@ -274,11 +274,11 @@
   in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end
 
 (* This assumes that distinct names are mapped to distinct names by
-   "Variable.variant_frees". This does not hold in general but should hold for
+   "Variable.variant_names". This does not hold in general but should hold for
    ATP-generated Skolem function names, since these end with a digit and
    "variant_frees" appends letters. *)
 fun desymbolize_and_fresh_up ctxt s =
-  fst (hd (Variable.variant_frees ctxt [] [(Name.desymbolize (SOME false) s, ())]))
+  fst (singleton (Variable.variant_names ctxt) (Name.desymbolize (SOME false) s, ()))
 
 (* 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". *)