diff -r d9ab86c044fd -r a12796872603 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Dec 19 15:47:17 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Dec 19 16:11:20 2013 +0100
@@ -87,8 +87,7 @@
 fun metis_call type_enc lam_trans =
   let
     val type_enc =
-      (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases
-                      type_enc of
+      (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
         [alias] => alias
       | _ => type_enc)
     val opts = [] |> type_enc <> partial_typesN ? cons type_enc
@@ -136,9 +135,8 @@
           (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018".
              Sometimes variables from the ATP are indistinguishable from Isabelle variables, which
              forces us to use a type parameter in all cases. *)
-          Type_Infer.param 0 (a |> perhaps (unprefix_and_unascii tvar_prefix),
-            (if null clss then HOLogic.typeS
-             else map class_of_atp_class clss))))
+          Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
+            (if null clss then HOLogic.typeS else map class_of_atp_class clss))))
   end
 
 fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us)