diff -r 96d5fa32f0f7 -r d7e0b6620c07 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Aug 19 05:49:16 2022 +0000
+++ b/src/HOL/Code_Numeral.thy	Fri Aug 19 05:49:17 2022 +0000
@@ -385,17 +385,17 @@
 where
   divmod_integer'_def: "divmod_integer m n = (numeral m div numeral n, numeral m mod numeral n)"
 
-definition divmod_step_integer :: "num \<Rightarrow> integer \<times> integer \<Rightarrow> integer \<times> integer"
+definition divmod_step_integer :: "integer \<Rightarrow> integer \<times> integer \<Rightarrow> integer \<times> integer"
 where
   "divmod_step_integer l qr = (let (q, r) = qr
-    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+    in if r \<ge> l then (2 * q + 1, r - l)
     else (2 * q, r))"
 
 instance proof
   show "divmod m n = (numeral m div numeral n :: integer, numeral m mod numeral n)"
     for m n by (fact divmod_integer'_def)
   show "divmod_step l qr = (let (q, r) = qr
-    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+    in if r \<ge> l then (2 * q + 1, r - l)
     else (2 * q, r))" for l and qr :: "integer \<times> integer"
     by (fact divmod_step_integer_def)
 qed (transfer,