--- 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)]