diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/Divides.thy	Mon Jul 12 10:48:37 2010 +0200
@@ -527,7 +527,7 @@
 begin
 
 definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
-  [code del]: "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
+  "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
 
 lemma divmod_nat_rel_divmod_nat:
   "divmod_nat_rel m n (divmod_nat m n)"