1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -1109,14 +1109,16 @@
     1.4    | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
     1.5                               maybe_nonmono_Ts, ...}
     1.6                         (Noninf_Nonmono_Types soundness) T =
     1.7 -    exists (type_instance ctxt T) maybe_nonmono_Ts andalso
     1.8 +    exists (type_instance ctxt T orf type_generalization ctxt T)
     1.9 +           maybe_nonmono_Ts andalso
    1.10      not (exists (type_instance ctxt T) surely_infinite_Ts orelse
    1.11           (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
    1.12            is_type_surely_infinite' ctxt soundness surely_infinite_Ts T))
    1.13    | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
    1.14                               maybe_nonmono_Ts, ...}
    1.15                         Fin_Nonmono_Types T =
    1.16 -    exists (type_instance ctxt T) maybe_nonmono_Ts andalso
    1.17 +    exists (type_instance ctxt T orf type_generalization ctxt T)
    1.18 +           maybe_nonmono_Ts andalso
    1.19      (exists (type_instance ctxt T) surely_finite_Ts orelse
    1.20       (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
    1.21        is_type_surely_finite ctxt T))