improve sort inference in Metis proofs -- in some rare cases Metis steals Isabelle's variable names and the sorts must then be inferred as well

--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jun 09 00:16:28 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jun 09 00:16:28 2011 +0200
@@ -387,11 +387,12 @@
       else case strip_prefix_and_unascii tfree_prefix a of
         SOME b => make_tfree ctxt b
       | NONE =>
-        case strip_prefix_and_unascii tvar_prefix a of
-          SOME b => make_tvar b
-        | NONE =>
-          (* Variable from the ATP, say "X1" *)
-          Type_Infer.param 0 (a, HOLogic.typeS)
+        (* 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. *)
+        (a |> perhaps (strip_prefix_and_unascii tvar_prefix), HOLogic.typeS)
+        |> Type_Infer.param 0
   end
 
 (* Type class literal applied to a type. Returns triple of polarity, class,