# HG changeset patch
# User blanchet
# Date 1335097006 -7200
# Node ID 13da7b50e9a5962589759b56004d9e6b24cab7c2
# Parent  b4f71d8aecd607b5280325fb64cac0ea4240ba18
more meaningful default value

diff -r b4f71d8aecd6 -r 13da7b50e9a5 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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])) =