--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Feb 18 18:48:07 2010 +0100
@@ -131,8 +131,7 @@
let
(* int -> int -> int -> KK.int_bound list *)
fun aux 0 _ _ = []
- | aux 1 pow_of_two j =
- if j < univ_card then [(SOME (~ pow_of_two), [single_atom j])] else []
+ | aux 1 pow_of_two j = [(SOME (~ pow_of_two), [single_atom j])]
| aux iter pow_of_two j =
(SOME pow_of_two, [single_atom j]) ::
aux (iter - 1) (2 * pow_of_two) (j + 1)