# HG changeset patch
# User blanchet
# Date 1303208579 -7200
# Node ID 9465651c0db7175cff201162126f5f047a6f809b
# Parent  252ed2fc384d53b6efc51173449176cb93e346e0
optimize trivial equalities early in Nitpick -- it shouldn't be the job of the peephole optimizer

diff -r 252ed2fc384d -r 9465651c0db7 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 19 12:21:57 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 19 12:22:59 2011 +0200
@@ -1066,7 +1066,11 @@
   | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1)
   | loose_bvar1_count _ = 0
 
-fun s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1'
+fun s_betapply _ (t1 as Const (@{const_name "=="}, _) $ t1', t2) =
+    if t1' aconv t2 then @{prop True} else t1 $ t2
+  | s_betapply _ (t1 as Const (@{const_name HOL.eq}, _) $ t1', t2) =
+    if t1' aconv t2 then @{term True} else t1 $ t2
+  | s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1'
   | s_betapply _ (Const (@{const_name If}, _) $ @{const False} $ _, t2) = t2
   | s_betapply Ts (Const (@{const_name Let},
                           Type (_, [bound_T, Type (_, [_, body_T])]))