# HG changeset patch
# User blanchet
# Date 1335097005 -7200
# Node ID b4f71d8aecd607b5280325fb64cac0ea4240ba18
# Parent  7a5c681c0265bae7e3abcf7195150b0e6ff65f7f
handle exception (needed to solve TPTP problem SEU880^5)

diff -r 7a5c681c0265 -r b4f71d8aecd6 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Apr 22 11:05:04 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Apr 22 14:16:45 2012 +0200
@@ -996,6 +996,7 @@
     in
       if k1 = max orelse k2 = max then max
       else Int.min (max, reasonable_power k2 k1)
+      handle TOO_LARGE _ => default_card
     end
   | bounded_card_of_type max default_card assigns
                          (Type (@{type_name prod}, [T1, T2])) =
diff -r 7a5c681c0265 -r b4f71d8aecd6 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Sun Apr 22 11:05:04 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sun Apr 22 14:16:45 2012 +0200
@@ -118,7 +118,8 @@
                  "negative exponent (" ^ signed_string_of_int b ^ ")")
     else if b > max_exponent then
       raise TOO_LARGE ("Nitpick_Util.reasonable_power",
-                       "too large exponent (" ^ signed_string_of_int b ^ ")")
+                       "too large exponent (" ^ signed_string_of_int a ^ " ^ " ^
+                       signed_string_of_int b ^ ")")
     else
       let val c = reasonable_power a (b div 2) in
         c * c * reasonable_power a (b mod 2)