--- 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 ())))