# HG changeset patch
# User blanchet
# Date 1281002093 -7200
# Node ID 8a9cace789d6c4da57bfac729fe660b7b03bdc96
# Parent  e26905526f7f719a7e720ad5423a82b15268dfad
deal correctly with Pure.conjunction in mono check

diff -r e26905526f7f -r 8a9cace789d6 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- 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