diff -r b51515722274 -r f602a380e4f2 src/HOL/Library/Tools/smt_word.ML --- a/src/HOL/Library/Tools/smt_word.ML Fri Jan 01 17:35:04 2021 +0100 +++ b/src/HOL/Library/Tools/smt_word.ML Fri Jan 01 23:35:09 2021 +0100 @@ -42,7 +42,7 @@ fun word_num (Type (\<^type_name>\word\, [T])) k = let val size = try dest_binT T - fun max_int size = IntInf.pow (2, size) + fun max_int size = Integer.pow size 2 in (case size of NONE => NONE