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