Incorrect result from signed right-shift when using Code_Target_Numeral

[Daniel Matichuk]

In Isabelle-2025-RC1 the following theory yields an incorrect result from
"value" (Hex_Words is optional):

*theory* "Scratch"
*imports* "HOL-Library.Word"  "HOL-Library.Code_Target_Numeral"
"Word_Lib.Hex_Words"
*begin*

*value* "signed_drop_bit 5 ((0x80000010 :: 32 word))"
(* "0xFC000001" :: "32 word" *)

*end*

However the correct result (0xFC000000) is given if Code_Target_Numeral is
not imported.

After some investigation I've determined that this is an issue that was
introduced in PolyML 5.6.2, which I've reported here:

https://github.com/polyml/polyml/issues/243
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251204/703378da/attachment.htm>