1.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jun 09 00:16:28 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jun 09 00:16:28 2011 +0200
     1.3 @@ -387,11 +387,12 @@
     1.4        else case strip_prefix_and_unascii tfree_prefix a of
     1.5          SOME b => make_tfree ctxt b
     1.6        | NONE =>
     1.7 -        case strip_prefix_and_unascii tvar_prefix a of
     1.8 -          SOME b => make_tvar b
     1.9 -        | NONE =>
    1.10 -          (* Variable from the ATP, say "X1" *)
    1.11 -          Type_Infer.param 0 (a, HOLogic.typeS)
    1.12 +        (* Could be an Isabelle variable or a variable from the ATP, say "X1"
    1.13 +           or "_5018". Sometimes variables from the ATP are indistinguishable
    1.14 +           from Isabelle variables, which forces us to use a type parameter in
    1.15 +           all cases. *)
    1.16 +        (a |> perhaps (strip_prefix_and_unascii tvar_prefix), HOLogic.typeS)
    1.17 +        |> Type_Infer.param 0
    1.18    end
    1.19  
    1.20  (* Type class literal applied to a type. Returns triple of polarity, class,