Incorrect result from signed right-shift when using Code_Target_Numeral

[Makarius]

On 06/12/2025 16:44, Florian Haftmann wrote:
> 
> It is interesting that this remained undiscovered – AFP session Native_Word 
> contains considerable tests for code generation for word types.
> 
> I’ll investigate what is missing there.

Maybe this version on isabelle-release helps:

changeset:   83716:4885450ab48d
tag:         tip
user:        wenzelm
date:        Sat Dec 06 23:01:40 2025 +0100
files:       src/Pure/ML/ml_init.ML
description:
expose bad IntInf shift operations in Poly/ML via explicit exceptions;


Testing it with afp-2025-1/3af26ffddf1b (-X slow) does not expose any errors, 
though.


	Makarius