src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 42414 9465651c0db7
parent 42361 23f352990944
child 42415 10accf397ab6
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 19 12:21:57 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 19 12:22:59 2011 +0200
     1.3 @@ -1066,7 +1066,11 @@
     1.4    | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1)
     1.5    | loose_bvar1_count _ = 0
     1.6  
     1.7 -fun s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1'
     1.8 +fun s_betapply _ (t1 as Const (@{const_name "=="}, _) $ t1', t2) =
     1.9 +    if t1' aconv t2 then @{prop True} else t1 $ t2
    1.10 +  | s_betapply _ (t1 as Const (@{const_name HOL.eq}, _) $ t1', t2) =
    1.11 +    if t1' aconv t2 then @{term True} else t1 $ t2
    1.12 +  | s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1'
    1.13    | s_betapply _ (Const (@{const_name If}, _) $ @{const False} $ _, t2) = t2
    1.14    | s_betapply Ts (Const (@{const_name Let},
    1.15                            Type (_, [bound_T, Type (_, [_, body_T])]))