src/HOL/Number_Theory/Totient.thy

                        "x mod m1 = y mod m1" "x mod m2 = y mod m2"
     have ex: "\<exists>!z. z < m1 * m2 \<and> [z = x] (mod m1) \<and> [z = x] (mod m2)"
       by (rule binary_chinese_remainder_unique_nat) (insert assms, simp_all)
     have "x < m1 * m2 \<and> [x = x] (mod m1) \<and> [x = x] (mod m2)"
          "y < m1 * m2 \<and> [y = x] (mod m1) \<and> [y = x] (mod m2)"
-      using xy assms by (simp_all add: totatives_less one_less_mult cong_nat_def)
+      using xy assms by (simp_all add: totatives_less one_less_mult cong_def)
     from this[THEN the1_equality[OF ex]] show "x = y" by simp
   qed
 next
   show "(\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1 * m2) = totatives m1 \<times> totatives m2"
   proof safe

       by (auto simp: totatives_def coprime_mul_eq not_le simp del: One_nat_def intro!: Nat.gr0I)
   next
     fix a b assume ab: "a \<in> totatives m1" "b \<in> totatives m2"
     with assms have ab': "a < m1" "b < m2" by (auto simp: totatives_less)
     with binary_chinese_remainder_unique_nat[OF assms(3), of a b] obtain x
-      where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_nat_def)
+      where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_def)
     from x ab assms(3) have "x \<in> totatives (m1 * m2)"
       by (auto simp: totatives_def coprime_mul_eq simp del: One_nat_def intro!: Nat.gr0I)
     with x show "(a, b) \<in> (\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1*m2)" by blast
   qed
 qed