1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Oct 29 22:16:12 2009 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Oct 29 22:16:40 2009 +0100
     1.3 @@ -54,15 +54,15 @@
     1.4    and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
     1.5  
     1.6  definition divmod_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
     1.7 -  [code del]: "divmod_aux = Divides.divmod"
     1.8 +  [code del]: "divmod_aux = divmod_nat"
     1.9  
    1.10  lemma [code]:
    1.11 -  "Divides.divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
    1.12 -  unfolding divmod_aux_def divmod_div_mod by simp
    1.13 +  "divmod_nat n m = (if m = 0 then (0, n) else divmod_aux n m)"
    1.14 +  unfolding divmod_aux_def divmod_nat_div_mod by simp
    1.15  
    1.16  lemma divmod_aux_code [code]:
    1.17    "divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"
    1.18 -  unfolding divmod_aux_def divmod_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
    1.19 +  unfolding divmod_aux_def divmod_nat_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
    1.20  
    1.21  lemma eq_nat_code [code]:
    1.22    "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"