author | blanchet |
Sun, 22 Apr 2012 14:16:46 +0200 | |
changeset 47668 | 13da7b50e9a5 |
parent 47667 | b4f71d8aecd6 |
child 47669 | f3896a53043f |
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Apr 22 14:16:45 2012 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Apr 22 14:16:46 2012 +0200 @@ -996,7 +996,7 @@ in if k1 = max orelse k2 = max then max else Int.min (max, reasonable_power k2 k1) - handle TOO_LARGE _ => default_card + handle TOO_LARGE _ => max end | bounded_card_of_type max default_card assigns (Type (@{type_name prod}, [T1, T2])) =