src/HOL/Library/RBT_Impl.thy
changeset 61433 a4c0de1df3d8
parent 61225 1a690dce8cfc
child 61585 a9599d3d7610
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Thu Oct 15 12:39:51 2015 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Sat Oct 17 13:18:43 2015 +0200
     1.3 @@ -1166,7 +1166,7 @@
     1.4      else if n = 1 then
     1.5        case kvs of (k, v) # kvs' \<Rightarrow> 
     1.6          (Branch R Empty k v Empty, kvs')
     1.7 -    else let (n', r) = divmod_nat n 2 in
     1.8 +    else let (n', r) = Divides.divmod_nat n 2 in
     1.9        if r = 0 then
    1.10          case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
    1.11            apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
    1.12 @@ -1177,7 +1177,7 @@
    1.13  lemma rbtreeify_g_code [code]:
    1.14    "rbtreeify_g n kvs =
    1.15     (if n = 0 \<or> n = 1 then (Empty, kvs)
    1.16 -    else let (n', r) = divmod_nat n 2 in
    1.17 +    else let (n', r) = Divides.divmod_nat n 2 in
    1.18        if r = 0 then
    1.19          case rbtreeify_g n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
    1.20            apfst (Branch B t1 k v) (rbtreeify_g n' kvs')