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