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