# HG changeset patch
# User wenzelm
# Date 1609540509 -3600
# Node ID f602a380e4f21c09411d9ab18b46d482a8deff04
# Parent  b51515722274e630ba335bb7af308d71cfce3868
tuned signature -- prefer Isabelle/ML structure Integer (despite minor confusion due to canonical argument order of "pow");

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>\<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