src/HOL/Tools/Nitpick/nitpick_hol.ML
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