don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
authorblanchet
Wed Feb 17 13:38:02 2010 +0100 (2010-02-17)
changeset 351873acab6c90d4a
parent 35186 bb64d089c643
child 35188 8c70a34931b1
don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 12:14:21 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 13:38:02 2010 +0100
     1.3 @@ -1019,8 +1019,8 @@
     1.4      val indexed_problems = if j >= 0 then
     1.5                               [(j, nth problems j)]
     1.6                             else
     1.7 -                             filter (is_problem_trivially_false o snd)
     1.8 -                                    (0 upto length problems - 1 ~~ problems)
     1.9 +                             filter_out (is_problem_trivially_false o snd)
    1.10 +                                        (0 upto length problems - 1 ~~ problems)
    1.11      val triv_js = filter_out (AList.defined (op =) indexed_problems)
    1.12                               (0 upto length problems - 1)
    1.13      (* int -> int *)
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Feb 17 12:14:21 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Feb 17 13:38:02 2010 +0100
     2.3 @@ -517,8 +517,7 @@
     2.4          | (Const (x as (s, T)), args) =>
     2.5            let val arg_Ts = binder_types T in
     2.6              if length arg_Ts = length args andalso
     2.7 -               (is_constr thy x orelse s = @{const_name Pair} orelse
     2.8 -                x = (@{const_name Suc}, nat_T --> nat_T)) andalso
     2.9 +               (is_constr thy x orelse s = @{const_name Pair}) andalso
    2.10                 (not careful orelse not (is_Var t1) orelse
    2.11                  String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
    2.12                discriminate_value hol_ctxt x t1 ::