gracefully handle the case where no integers occur in the formula and the "max" option is used

--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Jul 30 15:03:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Jul 30 18:28:18 2010 +0200
@@ -778,7 +778,8 @@
         val max_axiom =
           if honors_explicit_max then
             KK.True
-          else if is_twos_complement_representable bits (epsilon - delta) then
+          else if bits = 0 orelse
+               is_twos_complement_representable bits (epsilon - delta) then
             KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)
           else
             raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",