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