src/HOL/Tools/Nitpick/nitpick_peephole.ML
changeset 45398 7dbb7b044a11
parent 38126 8031d099379a
child 55889 6bfbec3dff62
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Nov 07 22:21:57 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Nov 07 22:22:01 2011 +0100
     1.3 @@ -358,8 +358,6 @@
     1.4        (case (r1, r2) of
     1.5           (Join (r11, Rel x), _) =>
     1.6           if x = not3_rel then s_rel_eq r11 (s_not3 r2) else raise SAME ()
     1.7 -       | (_, Join (r21, Rel x)) =>
     1.8 -         if x = not3_rel then s_rel_eq r21 (s_not3 r1) else raise SAME ()
     1.9         | (RelIf (f, r11, r12), _) =>
    1.10           if inline_rel_expr r2 then
    1.11             s_formula_if f (s_rel_eq r11 r2) (s_rel_eq r12 r2)