src/HOL/Tools/Nitpick/nitpick_peephole.ML
changeset 34936 c4f04bee79f3
parent 34126 8a2c5d7aff51
child 34982 7b8c366e34a2
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Thu Jan 14 17:06:35 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Wed Jan 20 10:38:06 2010 +0100
     1.3 @@ -421,8 +421,8 @@
     1.4          if is_one_rel_expr r1 then
     1.5            s_or (s_subset r1 r21) (s_subset r1 r22)
     1.6          else
     1.7 -          if s_subset r1 r21 = True orelse s_subset r1 r22 = True
     1.8 -             orelse r1 = r2 then
     1.9 +          if s_subset r1 r21 = True orelse s_subset r1 r22 = True orelse
    1.10 +             r1 = r2 then
    1.11              True
    1.12            else
    1.13              Subset (r1, r2)