src/HOL/Library/Tools/smt_word.ML
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