# HG changeset patch
# User blanchet
# Date 1280963532 -7200
# Node ID 4374005e02f9067758850cf4b2dd4bbaef2219ec
# Parent  51a1bfef9de238792a9cc6500831d8fc8ffbf0a2
remove buggy and needless condition

diff -r 51a1bfef9de2 -r 4374005e02f9 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Aug 05 00:21:11 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Aug 05 01:12:12 2010 +0200
@@ -839,7 +839,6 @@
                          (constr_ord = EQUAL andalso x = hd sel_xs) orelse
                          (T = dataT andalso
                           (no_direct orelse not (member (op =) sel_xs x)))))
-                                       (* FIXME: why the last disjunct above? *)
         fun subterms_r no_direct sel_xs j =
           loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa)
                            (filter_out (curry (op =) dataT) (map fst nfa)) dataT
@@ -861,12 +860,9 @@
                          EQUAL =>
                          kk_and
                              (lex_order_rel_expr kk dtypes (sel_quadruples2 ()))
-                             (if length rec_sel_xs2 > 1 then
-                                kk_all [KK.DeclOne ((1, 2),
-                                                    subterms_r true sel_xs1 0)]
-                                       (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2)))
-                              else
-                                KK.True)
+                             (kk_all [KK.DeclOne ((1, 2),
+                                                  subterms_r true sel_xs1 0)]
+                                     (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))))
                        | LESS =>
                          kk_all [KK.DeclOne ((1, 2),
                                  subterms_r false sel_xs1 0)]