1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 16 13:50:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 16 13:50:35 2011 +0200
     1.3 @@ -1656,11 +1656,6 @@
     1.4         ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
     1.5    end
     1.6  
     1.7 -(* These types witness that the type classes they belong to allow infinite
     1.8 -   models and hence that any types with these type classes is monotonic. *)
     1.9 -val known_infinite_types =
    1.10 -  [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
    1.11 -
    1.12  (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
    1.13     out with monotonicity" paper presented at CADE 2011. *)
    1.14  fun add_combterm_nonmonotonic_types _ _ _ (SOME false) _ = I
    1.15 @@ -1670,12 +1665,8 @@
    1.16      (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
    1.17       (case level of
    1.18          Noninf_Nonmono_Types =>
    1.19 -        (* Unlike virtually any other polymorphic fact whose type variables can
    1.20 -           be instantiated by a known infinite type, extensionality actually
    1.21 -           encodes a cardinality constraints. *)
    1.22          not (is_locality_global locality) orelse
    1.23 -        not (is_type_surely_infinite ctxt (if locality = Extensionality then []
    1.24 -                                           else known_infinite_types) T)
    1.25 +        not (is_type_surely_infinite ctxt T)
    1.26        | Fin_Nonmono_Types => is_type_surely_finite ctxt T
    1.27        | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
    1.28    | add_combterm_nonmonotonic_types _ _ _ _ _ = I