changeset 73021 | f602a380e4f2 |
parent 72909 | f9424ceea3c3 |
child 74097 | 6d7be1227d02 |
--- 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>\<open>word\<close>, [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