# HG changeset patch
# User blanchet
# Date 1291638789 -3600
# Node ID 343cdf923c023a8fb2b650def35059a3e94186bc
# Parent  3eeb25d953d24e0ede321988f9b20d35b54bc009
introduced hack to exploit the symmetry of equality in monotonicity calculus

diff -r 3eeb25d953d2 -r 343cdf923c02 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- 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)