diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Library/RBT_Impl.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -1154,24 +1154,24 @@
     else if n = 1 then
       case kvs of (k, v) # kvs' \<Rightarrow> 
         (Branch R Empty k v Empty, kvs')
-    else let (n', r) = Divides.divmod_nat n 2 in
+    else let (n', r) = Euclidean_Division.divmod_nat n 2 in
       if r = 0 then
         case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
       else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))"
-by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_def prod.case)
+by (subst rbtreeify_f.simps) (simp only: Let_def Euclidean_Division.divmod_nat_def prod.case)
 
 lemma rbtreeify_g_code [code]:
   "rbtreeify_g n kvs =
    (if n = 0 \<or> n = 1 then (Empty, kvs)
-    else let (n', r) = Divides.divmod_nat n 2 in
+    else let (n', r) = Euclidean_Division.divmod_nat n 2 in
       if r = 0 then
         case rbtreeify_g n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
       else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))"
-by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_def prod.case)
+by(subst rbtreeify_g.simps)(simp only: Let_def Euclidean_Division.divmod_nat_def prod.case)
 
 lemma Suc_double_half: "Suc (2 * n) div 2 = n"
 by simp