src/HOL/Tools/Nitpick/nitpick_preproc.ML

           if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
           else raise SAME ()
         | (Const (x as (s, T)), args) =>
           let val arg_Ts = binder_types T in
             if length arg_Ts = length args andalso
-               (is_constr thy x orelse s = @{const_name Pair} orelse
-                x = (@{const_name Suc}, nat_T --> nat_T)) andalso
+               (is_constr thy x orelse s = @{const_name Pair}) andalso
                (not careful orelse not (is_Var t1) orelse
                 String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
               discriminate_value hol_ctxt x t1 ::
               map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
               |> foldr1 s_conj