src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 47667 b4f71d8aecd6
parent 47433 07f4bf913230
child 47668 13da7b50e9a5
--- 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])) =