diff -r e61b0b819d28 -r bc758f4f09e5 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Sun Jan 13 20:25:41 2019 +0100
+++ b/src/HOL/Number_Theory/Gauss.thy	Mon Jan 14 14:46:12 2019 +0100
@@ -339,7 +339,7 @@
 theorem pre_gauss_lemma: "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
 proof -
   have "[prod id A = prod id F * prod id D](mod p)"
-    by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.cong_strong)
+    by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.cong_simp)
   then have "[prod id A = ((-1)^(card E) * prod id E) * prod id D] (mod p)"
     by (rule cong_trans) (metis cong_scalar_right prod_F_zcong)
   then have "[prod id A = ((-1)^(card E) * prod id C)] (mod p)"
@@ -364,7 +364,7 @@
       (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
     by (rule cong_trans) (simp add: a ac_simps)
   then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)"
-    by (rule cong_trans) (simp add: aux cong del: prod.cong_strong)
+    by (rule cong_trans) (simp add: aux cong del: prod.cong_simp)
   with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
     by (metis cong_mult_lcancel)
   then show ?thesis