diff -r 84c7cf36b2e0 -r eaa540986291 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jan 02 10:54:36 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jan 02 13:14:47 2013 +0100
@@ -77,8 +77,13 @@
                   |> lam_trans <> metis_default_lam_trans ? cons lam_trans
   in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
 
-fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
-fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
+fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
+  | term_name' t = ""
+
+fun lambda' v = Term.lambda_name (term_name' v, v)
+
+fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda' v t
+fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda' v t
 
 fun make_tfree ctxt w =
   let val ww = "'" ^ w in
@@ -248,7 +253,9 @@
                 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,
+                  Var ((s |> textual
+                          ? (repair_variable_name Char.toLower
+                             #> Char.isLower (String.sub (s, 0)) ? Name.skolem),
                         var_index), T)
           in list_comb (t, ts) end
   in do_term [] end