--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Aug 05 09:49:46 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Aug 05 11:54:53 2010 +0200
@@ -881,7 +881,9 @@
| Const (@{const_name Let}, _) $ t1 $ t2 =>
do_formula sn (betapply (t2, t1)) accum
| (t0 as Const (s0, _)) $ t1 $ t2 =>
- if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
+ if s0 = @{const_name "==>"} orelse
+ s0 = @{const_name Pure.conjunction} orelse
+ s0 = @{const_name "op &"} orelse
s0 = @{const_name "op |"} orelse
s0 = @{const_name "op -->"} then
let