# HG changeset patch
# User blanchet
# Date 1307571388 -7200
# Node ID 566f970006e5e1e4641cbc4bbfe086389ebdd0d9
# Parent  8d7fc4a5b50293c3d0a8865d30808d516886c597
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

diff -r 8d7fc4a5b502 -r 566f970006e5 src/HOL/Tools/ATP/atp_reconstruct.ML
--- 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,