1.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 24 18:35:21 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 24 18:36:18 2009 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4    * Optimized Kodkod encoding of datatypes whose constructors don't appear in
     1.5      the formula to falsify
     1.6    * Added support for codatatype view of datatypes
     1.7 +  * Fixed soundness bug in the "uncurry" optimization
     1.8    * Fixed soundness bugs related to sets, sets of sets, (co)inductive
     1.9      predicates, typedefs, "finite", "rel_comp", and negative literals
    1.10    * Fixed monotonicity check

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Nov 24 18:35:21 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Nov 24 18:36:18 2009 +0100
     2.3 @@ -1322,7 +1322,7 @@
     2.4                        (kk_rel_if (kk_or (kk_some (kk_join r1 true_atom))
     2.5                                          (kk_subset (full_rel_for_rep R)
     2.6                                                     (kk_join r1 false_atom)))
     2.7 -                                 (to_rep R u2) Kodkod.None)
     2.8 +                                 (to_rep R u2) (empty_rel_for_rep R))
     2.9            end
    2.10          else
    2.11            let val r1 = to_rep (Func (R, Formula Neut)) u1 in
    2.12 @@ -1335,20 +1335,20 @@
    2.13              val r2 = to_rep R u2
    2.14            in
    2.15              kk_union (kk_rel_if (kk_one (kk_join r1 true_atom))
    2.16 -                                (kk_join r1 true_atom) Kodkod.None)
    2.17 +                                (kk_join r1 true_atom) (empty_rel_for_rep R))
    2.18                       (kk_rel_if (kk_or (kk_subset r2 (kk_join r1 true_atom))
    2.19                                         (kk_subset (full_rel_for_rep R)
    2.20                                                    (kk_join r1 false_atom)))
    2.21 -                                r2 Kodkod.None)
    2.22 +                                r2 (empty_rel_for_rep R))
    2.23            end
    2.24          else
    2.25            let
    2.26              val r1 = to_rep (Func (unopt_rep R, Formula Neut)) u1
    2.27              val r2 = to_rep R u2
    2.28            in
    2.29 -            kk_union (kk_rel_if (kk_one r1) r1 Kodkod.None)
    2.30 +            kk_union (kk_rel_if (kk_one r1) r1 (empty_rel_for_rep R))
    2.31                       (kk_rel_if (kk_or (kk_no r1) (kk_subset r2 r1))
    2.32 -                                r2 Kodkod.None)
    2.33 +                                r2 (empty_rel_for_rep R))
    2.34            end
    2.35        | Op2 (Triad, T, Opt (Atom (2, j0)), u1, u2) =>
    2.36          let
    2.37 @@ -1754,8 +1754,10 @@
    2.38        else Kodkod.False
    2.39      (* nut -> Kodkod.rel_expr -> Kodkod.rel_expr *)
    2.40      and to_compare_with_unrep u r =
    2.41 -      if is_opt_rep (rep_of u) then kk_rel_if (kk_some (to_r u)) r Kodkod.None
    2.42 -      else r
    2.43 +      if is_opt_rep (rep_of u) then
    2.44 +        kk_rel_if (kk_some (to_r u)) r (empty_rel_for_rep (rep_of u))
    2.45 +      else
    2.46 +        r
    2.47    in to_f_with_polarity Pos u end
    2.48  
    2.49  end;