--- a/src/HOL/Old_Number_Theory/EulerFermat.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Mon Dec 28 01:28:28 2015 +0100
@@ -53,7 +53,7 @@
definition zcongm :: "int => int => int => bool"
where "zcongm m = (\<lambda>a b. zcong a b m)"
-lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
+lemma abs_eq_1_iff [iff]: "(\<bar>z\<bar> = (1::int)) = (z = 1 \<or> z = -1)"
-- \<open>LCP: not sure why this lemma is needed now\<close>
by (auto simp add: abs_if)