# HG changeset patch
# User blanchet
# Date 1304527705 -7200
# Node ID 223f01b32f172b055cd0c8bce0dfdf6b28294901
# Parent  593e375b939f50dae4ff67cfe1bf674dab0679b4
[mq]: nitpick_tuning

diff -r 593e375b939f -r 223f01b32f17 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed May 04 18:43:42 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed May 04 18:48:25 2011 +0200
@@ -980,6 +980,7 @@
                     handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
                            default_card)
 
+(* Similar to similarly named function in "Sledgehammer_ATP_Translate". *)
 fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
                                assigns T =
   let
@@ -990,24 +991,20 @@
          raise SAME ()
        else case T of
          Type (@{type_name fun}, [T1, T2]) =>
-         let
-           val k1 = aux avoid T1
-           val k2 = aux avoid T2
-         in
-           if k2 = 1 then 1
-           else if k1 = 0 orelse k2 = 0 then 0
-           else if k1 >= max orelse k2 >= max then max
-           else Int.min (max, reasonable_power k2 k1)
-         end
+         (case (aux avoid T1, aux avoid T2) of
+            (_, 1) => 1
+          | (0, _) => 0
+          | (_, 0) => 0
+          | (k1, k2) =>
+            if k1 >= max orelse k2 >= max then max
+            else Int.min (max, reasonable_power k2 k1))
        | Type (@{type_name prod}, [T1, T2]) =>
-         let
-           val k1 = aux avoid T1
-           val k2 = aux avoid T2
-         in
-           if k1 = 0 orelse k2 = 0 then 0
-           else if k1 >= max orelse k2 >= max then max
-           else Int.min (max, k1 * k2)
-         end
+         (case (aux avoid T1, aux avoid T2) of
+            (0, _) => 0
+          | (_, 0) => 0
+          | (k1, k2) =>
+            if k1 >= max orelse k2 >= max then max
+            else Int.min (max, k1 * k2))
        | Type (@{type_name itself}, _) => 1
        | @{typ prop} => 2
        | @{typ bool} => 2
@@ -1022,7 +1019,7 @@
                     constrs
             in
               if exists (curry (op =) 0) constr_cards then 0
-              else Integer.sum constr_cards
+              else Int.min (max, Integer.sum constr_cards)
             end)
        | _ => raise SAME ())
       handle SAME () =>