# HG changeset patch
# User desharna
# Date 1743175059 -3600
# Node ID 3c3ae21cf12d6de4bfb17d6a5c01be91b96b777a
# Parent  eae75676ecd7a5721659e68fa7777499f30da636# Parent  07e95760a612dd34067fe8cabdbe17384ea13b53
merged

diff -r eae75676ecd7 -r 3c3ae21cf12d src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Fri Mar 28 16:11:05 2025 +0100
+++ b/src/HOL/Library/Word.thy	Fri Mar 28 16:17:39 2025 +0100
@@ -475,9 +475,10 @@
   by (rule; transfer) simp
 
 lemma [code]:
-  \<open>Word.the_signed_int w = signed_take_bit (LENGTH('a) - Suc 0) (Word.the_int w)\<close>
+  \<open>Word.the_signed_int w = (let k = Word.the_int w
+    in if bit k (LENGTH('a) - Suc 0) then k + push_bit LENGTH('a) (- 1) else k)\<close>
   for w :: \<open>'a::len word\<close>
-  by transfer (simp add: signed_take_bit_take_bit)
+  by transfer (simp add: bit_simps signed_take_bit_eq_take_bit_add)
 
 lemma [code_abbrev, simp]:
   \<open>Word.the_signed_int = sint\<close>