# HG changeset patch
# User blanchet
# Date 1695654992 -7200
# Node ID 8ca71c0ae31f669dc794a383dcb7dacd56176588
# Parent  ef89f1beee951cf29096c825a3c85faf8e8b4235
avoid legacy binding errors in Sledgehammer Isar proofs

diff -r ef89f1beee95 -r 8ca71c0ae31f src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Sep 25 17:16:32 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Sep 25 17:16:32 2023 +0200
@@ -257,10 +257,12 @@
       | norm_var_types t = t
   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 ATP-generated Skolem function names, since these end
-   with a digit and "variant_frees" appends letters. *)
-fun fresh_up ctxt s = fst (hd (Variable.variant_frees ctxt [] [(s, ())]))
+(* This assumes that distinct names are mapped to distinct names by
+   "Variable.variant_frees". 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, ())]))
 
 (* 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". *)
@@ -346,7 +348,7 @@
                 (case unprefix_and_unascii fixed_var_prefix s of
                   SOME s => Free (s, T)
                 | NONE =>
-                  if not (is_tptp_variable s) then Free (fresh_up ctxt s, T)
+                  if not (is_tptp_variable s) then Free (desymbolize_and_fresh_up ctxt s, T)
                   else Var ((repair_var_name s, var_index), T))
             in list_comb (t, ts) end))
   in do_term end
@@ -437,7 +439,7 @@
                   SOME s => Free (s, T)
                 | NONE =>
                   if textual andalso not (is_tptp_variable s) then
-                    Free (s |> textual ? fresh_up ctxt, T)
+                    Free (desymbolize_and_fresh_up ctxt s, T)
                   else
                     Var ((repair_var_name s, var_index), T))
             in list_comb (t, ts) end))