# HG changeset patch
# User blanchet
# Date 1323784542 -3600
# Node ID 0b19934792d2c9083364f55836f3fb085f630053
# Parent  3b8606fba2ddb235da4be2a76bac81952a304fcd
remove needless declaration in TFF1 problems

diff -r 3b8606fba2dd -r 0b19934792d2 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 13 14:55:42 2011 +0100
@@ -2022,7 +2022,9 @@
     |> is_type_enc_fairly_sound type_enc
        ? (fold (fold add_fact_syms) [conjs, facts]
           #> (case type_enc of
-                Simple_Types (First_Order, Polymorphic, _) => add_TYPE_const ()
+                Simple_Types (First_Order, Polymorphic, _) =>
+                if avoid_first_order_ghost_type_vars then add_TYPE_const ()
+                else I
               | Simple_Types _ => I
               | _ => fold add_undefined_const (var_types ())))
   end