src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 35187 3acab6c90d4a
parent 35079 592edca1dfb3
child 35190 ce653cc27a94
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Feb 17 12:14:21 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Feb 17 13:38:02 2010 +0100
     1.3 @@ -517,8 +517,7 @@
     1.4          | (Const (x as (s, T)), args) =>
     1.5            let val arg_Ts = binder_types T in
     1.6              if length arg_Ts = length args andalso
     1.7 -               (is_constr thy x orelse s = @{const_name Pair} orelse
     1.8 -                x = (@{const_name Suc}, nat_T --> nat_T)) andalso
     1.9 +               (is_constr thy x orelse s = @{const_name Pair}) andalso
    1.10                 (not careful orelse not (is_Var t1) orelse
    1.11                  String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
    1.12                discriminate_value hol_ctxt x t1 ::