# HG changeset patch
# User blanchet
# Date 1407225755 -7200
# Node ID a04e8a39ca9accb0c5c33bdddf9dfd94733bee68
# Parent  a73255cffb5b1ce57cb565442e8eda9f1af8025f
tuned code

diff -r a73255cffb5b -r a04e8a39ca9a src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Aug 05 09:58:23 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Aug 05 10:02:35 2014 +0200
@@ -224,14 +224,20 @@
 
 fun quantify_over_var textual quant_of var_s var_T t =
   let
-    val vars = ((var_s, var_index_of_textual textual), var_T) ::
-                 filter (fn ((s, _), _) => s = var_s) (Term.add_vars t [])
+    val vars =
+      ((var_s, var_index_of_textual textual), var_T) ::
+      filter (fn ((s, _), _) => s = var_s) (Term.add_vars t [])
     val normTs = vars |> AList.group (op =) |> map (apsnd hd)
     fun norm_var_types (Var (x, T)) =
         Var (x, the_default T (AList.lookup (op =) normTs x))
       | 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, ())]))
+
 (* 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". *)
 fun term_of_atp_ho ctxt sym_tab =
@@ -295,8 +301,6 @@
             in list_comb (t, term_ts) end
           | NONE => (* a free or schematic variable *)
             let
-              fun fresh_up s =
-                [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
               val ts = map (do_term NONE) us
               val T =
                 (case opt_T of
@@ -310,7 +314,7 @@
                 (case unprefix_and_unascii fixed_var_prefix s of
                   SOME s => Free (s, T)
                 | NONE =>
-                  if not (is_tptp_variable s) then Free (s |> fresh_up, T)
+                  if not (is_tptp_variable s) then Free (fresh_up ctxt s, T)
                   else Var ((repair_var_name s, var_index), T))
             in list_comb (t, ts) end))
   in do_term end
@@ -382,12 +386,6 @@
             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
                 (* SPASS (3.8ds) and Vampire (2.6) pass arguments to Skolem functions in reverse
@@ -406,7 +404,7 @@
                   SOME s => Free (s, T)
                 | NONE =>
                   if textual andalso not (is_tptp_variable s) then
-                    Free (s |> textual ? fresh_up, T)
+                    Free (s |> textual ? fresh_up ctxt, T)
                   else
                     Var ((repair_var_name s, var_index), T))
             in list_comb (t, ts) end))