# HG changeset patch
# User blanchet
# Date 1266410282 -3600
# Node ID 3acab6c90d4a91f6f8eb54cd5c8a70f66fd8d42d
# Parent  bb64d089c643ab621162bc0b1326de2c428cbc3d
don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)

diff -r bb64d089c643 -r 3acab6c90d4a src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 12:14:21 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 13:38:02 2010 +0100
@@ -1019,8 +1019,8 @@
     val indexed_problems = if j >= 0 then
                              [(j, nth problems j)]
                            else
-                             filter (is_problem_trivially_false o snd)
-                                    (0 upto length problems - 1 ~~ problems)
+                             filter_out (is_problem_trivially_false o snd)
+                                        (0 upto length problems - 1 ~~ problems)
     val triv_js = filter_out (AList.defined (op =) indexed_problems)
                              (0 upto length problems - 1)
     (* int -> int *)
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 ::