diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/Library/Code_Binary_Nat.thy
--- a/src/HOL/Library/Code_Binary_Nat.thy	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Library/Code_Binary_Nat.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -127,13 +127,13 @@
   "nat_of_num k < nat_of_num l \<longleftrightarrow> k < l"
   by (simp_all add: nat_of_num_numeral)
 
-declare [[code drop: Divides.divmod_nat]]
+declare [[code drop: Euclidean_Division.divmod_nat]]
   
 lemma divmod_nat_code [code]:
-  "Divides.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
-  "Divides.divmod_nat m 0 = (0, m)"
-  "Divides.divmod_nat 0 n = (0, 0)"
-  by (simp_all add: prod_eq_iff nat_of_num_numeral)
+  "Euclidean_Division.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
+  "Euclidean_Division.divmod_nat m 0 = (0, m)"
+  "Euclidean_Division.divmod_nat 0 n = (0, 0)"
+  by (simp_all add: Euclidean_Division.divmod_nat_def nat_of_num_numeral)
 
 end