diff -r 2fab72ab919a -r cb504351d058 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Tue Nov 05 19:55:42 2019 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Tue Nov 05 21:07:03 2019 +0100
@@ -135,8 +135,7 @@
       by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
     have "CARD('a) ^ CARD('b) = card (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
       (is "_ = card ?A")
-      by (subst card_PiE) (auto simp: prod_constant)
-    
+      by (subst card_PiE) (auto)
     also have "?A = Pi UNIV (\<lambda>_. UNIV)" 
       by auto
     finally show "card \<dots> = CARD('a) ^ CARD('b)" ..
@@ -1075,7 +1074,7 @@
 
 lemma matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
   apply (vector matrix_vector_mult_def mat_def)
-  apply (simp add: if_distrib if_distribR sum.delta' cong del: if_weak_cong)
+  apply (simp add: if_distrib if_distribR cong del: if_weak_cong)
   done
 
 lemma matrix_transpose_mul: