fixed cardinality computation for function types such as "'a -> unit"
authorblanchet
Wed May 04 18:43:42 2011 +0200 (2011-05-04)
changeset 42678593e375b939f
parent 42677 25496cd3c199
child 42679 223f01b32f17
fixed cardinality computation for function types such as "'a -> unit"
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed May 04 15:35:05 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed May 04 18:43:42 2011 +0200
     1.3 @@ -994,7 +994,8 @@
     1.4             val k1 = aux avoid T1
     1.5             val k2 = aux avoid T2
     1.6           in
     1.7 -           if k1 = 0 orelse k2 = 0 then 0
     1.8 +           if k2 = 1 then 1
     1.9 +           else if k1 = 0 orelse k2 = 0 then 0
    1.10             else if k1 >= max orelse k2 >= max then max
    1.11             else Int.min (max, reasonable_power k2 k1)
    1.12           end