# HG changeset patch
# User blanchet
# Date 1403590796 -7200
# Node ID d20cf3ec7fa73e39d13a1479769443261aca7094
# Parent  1bac14e0a7289535674795f45b83c3cdc15dfc8d
phantoms may also occur in THF1

diff -r 1bac14e0a728 -r d20cf3ec7fa7 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 24 08:19:55 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 24 08:19:56 2014 +0200
@@ -969,7 +969,7 @@
     val tm_args =
       tm_args @
       (case type_enc of
-        Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
+        Native (_, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
         [ATerm ((TYPE_name, ty_args), [])]
       | _ => [])
   in AAtom (ATerm ((cl, ty_args), tm_args)) end
@@ -2196,7 +2196,7 @@
        ? (fold (fold add_fact_syms) [conjs, facts]
           #> fold add_iterm_syms extra_tms
           #> (case type_enc of
-                Native (First_Order, Raw_Polymorphic phantoms, _) =>
+                Native (_, Raw_Polymorphic phantoms, _) =>
                 phantoms = Without_Phantom_Type_Vars ? add_TYPE_const ()
               | Native _ => I
               | _ => fold add_undefined_const (var_types ())))