diff -r 5689f0db4508 -r 759532ef0885 src/HOL/Word/Bit_Comprehension.thy
--- a/src/HOL/Word/Bit_Comprehension.thy	Sun Jul 12 18:10:06 2020 +0000
+++ b/src/HOL/Word/Bit_Comprehension.thy	Sun Jul 12 18:10:06 2020 +0000
@@ -18,10 +18,10 @@
   "set_bits f =
     (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
       let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
-      in bl_to_bin (rev (map f [0..<n]))
+      in horner_sum of_bool 2 (map f [0..<n])
      else if \<exists>n. \<forall>n'\<ge>n. f n' then
       let n = LEAST n. \<forall>n'\<ge>n. f n'
-      in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
+      in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True]))
      else 0 :: int)"
 
 instance ..