changeset 42678 | 593e375b939f |
parent 42425 | 2aa907d5ee4f |
child 42679 | 223f01b32f17 |
--- 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