diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Num.thy --- a/src/HOL/Num.thy Tue May 23 20:11:15 2023 +0200 +++ b/src/HOL/Num.thy Tue May 23 21:43:36 2023 +0200 @@ -1394,7 +1394,7 @@ \ simproc_setup reorient_numeral ("numeral w = x" | "- numeral w = y") = - Reorient_Proc.proc + \K Reorient_Proc.proc\ subsubsection \Simplification of arithmetic operations on integer constants\