# HG changeset patch
# User blanchet
# Date 1314018165 -7200
# Node ID 8801a1eef30a63279ee6051c20f9bcd9277da9e5
# Parent  b529d9501d64686e4cacc900567b9e954db6b5d6
we must tag any type whose ground types intersect a nonmonotonic type

diff -r b529d9501d64 -r 8801a1eef30a src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -1109,14 +1109,16 @@
   | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
                              maybe_nonmono_Ts, ...}
                        (Noninf_Nonmono_Types soundness) T =
-    exists (type_instance ctxt T) maybe_nonmono_Ts andalso
+    exists (type_instance ctxt T orf type_generalization ctxt T)
+           maybe_nonmono_Ts andalso
     not (exists (type_instance ctxt T) surely_infinite_Ts orelse
          (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
           is_type_surely_infinite' ctxt soundness surely_infinite_Ts T))
   | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
                              maybe_nonmono_Ts, ...}
                        Fin_Nonmono_Types T =
-    exists (type_instance ctxt T) maybe_nonmono_Ts andalso
+    exists (type_instance ctxt T orf type_generalization ctxt T)
+           maybe_nonmono_Ts andalso
     (exists (type_instance ctxt T) surely_finite_Ts orelse
      (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
       is_type_surely_finite ctxt T))