src/HOL/Number_Theory/Gauss.thy

--- a/src/HOL/Number_Theory/Gauss.thy	Fri Oct 10 18:23:59 2014 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Thu Oct 09 22:43:48 2014 +0200
@@ -57,7 +57,7 @@
 
 lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
   using odd_p p_ge_2
-  by (auto simp add: even_def) (metis p_eq2)
+  by (auto simp add: even_iff_mod_2_eq_zero) (metis p_eq2)
 
 
 subsection {* Basic Properties of the Gauss Sets *}