# HG changeset patch
# User blanchet
# Date 1357167735 -3600
# Node ID 2fac44deb8b515f4caaa76984b50058166e8ded6
# Parent  97f951edca46fa81d12722957e68933dd0a6c132
tuned comment

diff -r 97f951edca46 -r 2fac44deb8b5 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jan 02 22:16:16 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jan 03 00:02:15 2013 +0100
@@ -240,6 +240,10 @@
           end
         | NONE => (* a free or schematic variable *)
           let
+            (* 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 s =
               [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
             val term_ts = map (do_term [] NONE) us