diff -r bb64d089c643 -r 3acab6c90d4a src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Feb 17 12:14:21 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Feb 17 13:38:02 2010 +0100 @@ -517,8 +517,7 @@ | (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 ::