diff -r e3e707c8ac57 -r 83b8a5a39709 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jan 02 16:32:40 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jan 02 19:59:06 2013 +0100
@@ -128,10 +128,10 @@
   | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
   | add_type_constraint _ _ = I
 
-fun repair_variable_name f s =
+fun repair_var_name s =
   let
     fun subscript_name s n = s ^ nat_subscript n
-    val s = String.map f s
+    val s = String.map Char.toLower s
   in
     case space_explode "_" s of
       [_] => (case take_suffix Char.isDigit (String.explode s) of
@@ -240,6 +240,8 @@
           end
         | NONE => (* a free or schematic variable *)
           let
+            fun fresh_up s =
+              [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
             val term_ts = map (do_term [] NONE) us
             val ts = term_ts @ extra_ts
             val T =
@@ -253,10 +255,10 @@
                 case unprefix_and_unascii schematic_var_prefix s of
                   SOME s => Var ((s, var_index), T)
                 | NONE =>
-                  Var ((s |> textual
-                          ? (repair_variable_name Char.toLower
-                             #> Char.isLower (String.sub (s, 0)) ? Name.skolem),
-                        var_index), T)
+                  if textual andalso not (is_tptp_variable s) then
+                    Free (s |> textual ? (repair_var_name #> fresh_up), T)
+                  else
+                    Var ((s |> textual ? repair_var_name, var_index), T)
           in list_comb (t, ts) end
   in do_term [] end
 
@@ -301,7 +303,7 @@
         (* FIXME: TFF *)
         #>> quantify_over_var
               (case q of AForall => forall_of | AExists => exists_of)
-              (s |> textual ? repair_variable_name Char.toLower)
+              (s |> textual ? repair_var_name)
       | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
       | AConn (c, [phi1, phi2]) =>
         do_formula (pos |> c = AImplies ? not) phi1