introduced hack to exploit the symmetry of equality in monotonicity calculus

--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
@@ -852,6 +852,10 @@
          (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
        | @{const True} =>
          (MRaw (t, bool_M), accum ||> add_comp_frame (A Tru) Leq frame)
+       | (t0 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t2 =>
+         (* hack to exploit symmetry of equality when typing "insert" *)
+         (if t2 = Bound 0 then do_term @{term True}
+          else do_term (t0 $ t2 $ Bound 0)) accum
        | Const (x as (s, T)) =>
          (case AList.lookup (op =) consts x of
             SOME M => (M, accum)