1.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Aug 05 00:21:11 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Aug 05 01:12:12 2010 +0200
     1.3 @@ -839,7 +839,6 @@
     1.4                           (constr_ord = EQUAL andalso x = hd sel_xs) orelse
     1.5                           (T = dataT andalso
     1.6                            (no_direct orelse not (member (op =) sel_xs x)))))
     1.7 -                                       (* FIXME: why the last disjunct above? *)
     1.8          fun subterms_r no_direct sel_xs j =
     1.9            loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa)
    1.10                             (filter_out (curry (op =) dataT) (map fst nfa)) dataT
    1.11 @@ -861,12 +860,9 @@
    1.12                           EQUAL =>
    1.13                           kk_and
    1.14                               (lex_order_rel_expr kk dtypes (sel_quadruples2 ()))
    1.15 -                             (if length rec_sel_xs2 > 1 then
    1.16 -                                kk_all [KK.DeclOne ((1, 2),
    1.17 -                                                    subterms_r true sel_xs1 0)]
    1.18 -                                       (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2)))
    1.19 -                              else
    1.20 -                                KK.True)
    1.21 +                             (kk_all [KK.DeclOne ((1, 2),
    1.22 +                                                  subterms_r true sel_xs1 0)]
    1.23 +                                     (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))))
    1.24                         | LESS =>
    1.25                           kk_all [KK.DeclOne ((1, 2),
    1.26                                   subterms_r false sel_xs1 0)]