--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Jan 20 10:38:19 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Jan 20 11:54:19 2010 +0100
@@ -320,8 +320,8 @@
val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
(* typ -> bool *)
fun is_type_always_monotonic T =
- ((not (is_pure_typedef thy T) orelse is_univ_typedef thy T) andalso
- not (is_quot_type thy T)) orelse
+ (is_datatype thy T andalso not (is_quot_type thy T) andalso
+ (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
is_number_type thy T orelse is_bit_type T
fun is_type_monotonic T =
unique_scope orelse