src/HOL/Tools/Nitpick/nitpick.ML
changeset 40993 52ee2a187cdb
parent 40411 36b7ed41ca9f
child 41001 11715564e2ad
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 06 13:18:25 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 06 13:18:25 2010 +0100
     1.3 @@ -347,7 +347,7 @@
     1.4         (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
     1.5        is_number_type ctxt T orelse is_bit_type T
     1.6      fun is_type_actually_monotonic T =
     1.7 -      formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
     1.8 +      formulas_monotonic hol_ctxt binarize 3 T (nondef_ts, def_ts)
     1.9      fun is_type_kind_of_monotonic T =
    1.10        case triple_lookup (type_match thy) monos T of
    1.11          SOME (SOME false) => false