# HG changeset patch
# User blanchet
# Date 1343895029 -7200
# Node ID ee9cba42d83d58cdfa48e0efa5f902a90c749f09
# Parent  6ac7fd9b3a54e8cc63f372a2106dac102515125a
don't tag negatively naked variables

diff -r 6ac7fd9b3a54 -r ee9cba42d83d src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Aug 02 10:10:29 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Aug 02 10:10:29 2012 +0200
@@ -154,6 +154,9 @@
   Guards of polymorphism * type_level |
   Tags of polymorphism * type_level
 
+(* not clear whether ATPs prefer to have their negative variables tagged *)
+val tag_neg_vars = false
+
 fun is_type_enc_native (Native _) = true
   | is_type_enc_native _ = false
 fun is_type_enc_higher_order (Native (Higher_Order _, _, _)) = true
@@ -1418,7 +1421,9 @@
       case level of
         Nonmono_Types (_, Non_Uniform) =>
         (case (site, is_maybe_universal_var u) of
-           (Eq_Arg _, true) => should_encode_type ctxt mono level T
+           (Eq_Arg pos, true) =>
+           (pos <> SOME false orelse tag_neg_vars) andalso
+           should_encode_type ctxt mono level T
          | _ => false)
       | Undercover_Types =>
         (case (site, is_maybe_universal_var u) of