src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Mon Nov 06 16:28:30 2006 +0100
+++ b/src/HOL/Divides.thy	Mon Nov 06 16:28:31 2006 +0100
@@ -896,10 +896,8 @@
   "m mod n = snd (divmod m n)"
   unfolding divmod_def by simp
 
-code_constname
-  "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.div_nat"
-  "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.mod_nat"
-  Divides.divmod "IntDef.divmod_nat"
+code_modulename SML
+  Divides Integer
 
 hide (open) const divmod