# 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,