src/HOL/Tools/Nitpick/nitpick.ML

     fun is_type_fundamentally_monotonic T =
       (is_datatype ctxt stds T andalso not (is_quot_type ctxt T) andalso
        (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
       is_number_type ctxt T orelse is_bit_type T
     fun is_type_actually_monotonic T =
-      formulas_monotonic hol_ctxt binarize 3 T (nondef_ts, def_ts)
+      formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
     fun is_type_kind_of_monotonic T =
       case triple_lookup (type_match thy) monos T of
         SOME (SOME false) => false
       | _ => is_type_actually_monotonic T
     fun is_type_monotonic T =