src/HOL/Tools/Nitpick/nitpick_util.ML
changeset 47667 b4f71d8aecd6
parent 46711 f745bcc4a1e5
child 48323 7b5f7ca25d17
equal deleted inserted replaced
47660:7a5c681c0265 47667:b4f71d8aecd6
   116     if b < 0 then
   116     if b < 0 then
   117       raise ARG ("Nitpick_Util.reasonable_power",
   117       raise ARG ("Nitpick_Util.reasonable_power",
   118                  "negative exponent (" ^ signed_string_of_int b ^ ")")
   118                  "negative exponent (" ^ signed_string_of_int b ^ ")")
   119     else if b > max_exponent then
   119     else if b > max_exponent then
   120       raise TOO_LARGE ("Nitpick_Util.reasonable_power",
   120       raise TOO_LARGE ("Nitpick_Util.reasonable_power",
   121                        "too large exponent (" ^ signed_string_of_int b ^ ")")
   121                        "too large exponent (" ^ signed_string_of_int a ^ " ^ " ^
       
   122                        signed_string_of_int b ^ ")")
   122     else
   123     else
   123       let val c = reasonable_power a (b div 2) in
   124       let val c = reasonable_power a (b div 2) in
   124         c * c * reasonable_power a (b mod 2)
   125         c * c * reasonable_power a (b mod 2)
   125       end
   126       end
   126 
   127