--- a/src/HOL/Library/Efficient_Nat.thy Wed Jan 28 11:04:45 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Wed Jan 28 13:36:11 2009 +0100
@@ -56,10 +56,10 @@
and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
definition divmod_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
- [code del]: "divmod_aux = divmod"
+ [code del]: "divmod_aux = Divides.divmod"
lemma [code]:
- "divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
+ "Divides.divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
unfolding divmod_aux_def divmod_div_mod by simp
lemma divmod_aux_code [code]: