# HG changeset patch
# User blanchet
# Date 1304527422 -7200
# Node ID 593e375b939f50dae4ff67cfe1bf674dab0679b4
# Parent  25496cd3c199a10a010e52efe5f4eb58ef24a086
fixed cardinality computation for function types such as "'a -> unit"

diff -r 25496cd3c199 -r 593e375b939f src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed May 04 15:35:05 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed May 04 18:43:42 2011 +0200
@@ -994,7 +994,8 @@
            val k1 = aux avoid T1
            val k2 = aux avoid T2
          in
-           if k1 = 0 orelse k2 = 0 then 0
+           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