src/HOL/Product_Type.thy

--- a/src/HOL/Product_Type.thy	Mon Mar 18 15:35:34 2019 +0000
+++ b/src/HOL/Product_Type.thy	Tue Mar 19 16:14:51 2019 +0000
@@ -1124,7 +1124,7 @@
 lemma vimage_snd: "snd -` A = UNIV \<times> A"
   by auto
 
-lemma insert_times_insert [simp]:
+lemma insert_Times_insert [simp]:
   "insert a A \<times> insert b B = insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
   by blast