--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Dec 06 13:18:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Dec 06 13:18:25 2010 +0100
@@ -347,7 +347,7 @@
(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 T (nondef_ts, def_ts)
+ formulas_monotonic hol_ctxt binarize 3 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