src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 38199 8a9cace789d6
parent 38190 b02e204b613a
child 38786 e46e7a9cb622
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Aug 05 09:49:46 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Aug 05 11:54:53 2010 +0200
     1.3 @@ -881,7 +881,9 @@
     1.4             | Const (@{const_name Let}, _) $ t1 $ t2 =>
     1.5               do_formula sn (betapply (t2, t1)) accum
     1.6             | (t0 as Const (s0, _)) $ t1 $ t2 =>
     1.7 -             if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
     1.8 +             if s0 = @{const_name "==>"} orelse
     1.9 +                s0 = @{const_name Pure.conjunction} orelse
    1.10 +                s0 = @{const_name "op &"} orelse
    1.11                  s0 = @{const_name "op |"} orelse
    1.12                  s0 = @{const_name "op -->"} then
    1.13                 let