1.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Nov 13 15:59:53 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Nov 17 19:47:27 2009 +0100
     1.3 @@ -1092,6 +1092,12 @@
     1.4                    else
     1.5                      kk_rel_eq r1 r2
     1.6                  end)
     1.7 +         | Op2 (The, T, _, u1, u2) =>
     1.8 +           to_f_with_polarity polar
     1.9 +                              (Op2 (The, T, Opt (Atom (2, bool_j0)), u1, u2))
    1.10 +         | Op2 (Eps, T, _, u1, u2) =>
    1.11 +           to_f_with_polarity polar
    1.12 +                              (Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2))
    1.13           | Op2 (Apply, T, _, u1, u2) =>
    1.14             (case (polar, rep_of u1) of
    1.15                (Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1)