src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Mon Feb 21 10:42:29 2011 +0100
+++ b/src/HOL/Divides.thy	Mon Feb 21 10:44:19 2011 +0100
@@ -2470,9 +2470,7 @@
     in subst [OF mod_div_equality [of _ n]])
    arith
 
-lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
-                       mod_div_equality' [THEN eq_reflection]
-                       zmod_zdiv_equality' [THEN eq_reflection]
+lemmas [nitpick_unfold] = dvd_eq_mod_eq_0 mod_div_equality' zmod_zdiv_equality'
 
 
 subsubsection {* Code generation *}