src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41016 343cdf923c02
parent 41014 e538a4f9dd86
child 41017 666d8ed0b73a
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -852,6 +852,10 @@
     1.4           (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
     1.5         | @{const True} =>
     1.6           (MRaw (t, bool_M), accum ||> add_comp_frame (A Tru) Leq frame)
     1.7 +       | (t0 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t2 =>
     1.8 +         (* hack to exploit symmetry of equality when typing "insert" *)
     1.9 +         (if t2 = Bound 0 then do_term @{term True}
    1.10 +          else do_term (t0 $ t2 $ Bound 0)) accum
    1.11         | Const (x as (s, T)) =>
    1.12           (case AList.lookup (op =) consts x of
    1.13              SOME M => (M, accum)