src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/Divides.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -131,7 +131,7 @@
   note that ultimately show thesis by blast
 qed
 
-lemma dvd_eq_mod_eq_0 [code, code_unfold, code_inline del]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
 proof
   assume "b mod a = 0"
   with mod_div_equality [of b a] have "b div a * a = b" by simp