1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 24 08:19:55 2014 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 24 08:19:56 2014 +0200
     1.3 @@ -969,7 +969,7 @@
     1.4      val tm_args =
     1.5        tm_args @
     1.6        (case type_enc of
     1.7 -        Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
     1.8 +        Native (_, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
     1.9          [ATerm ((TYPE_name, ty_args), [])]
    1.10        | _ => [])
    1.11    in AAtom (ATerm ((cl, ty_args), tm_args)) end
    1.12 @@ -2196,7 +2196,7 @@
    1.13         ? (fold (fold add_fact_syms) [conjs, facts]
    1.14            #> fold add_iterm_syms extra_tms
    1.15            #> (case type_enc of
    1.16 -                Native (First_Order, Raw_Polymorphic phantoms, _) =>
    1.17 +                Native (_, Raw_Polymorphic phantoms, _) =>
    1.18                  phantoms = Without_Phantom_Type_Vars ? add_TYPE_const ()
    1.19                | Native _ => I
    1.20                | _ => fold add_undefined_const (var_types ())))