diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Coset.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -1379,7 +1379,7 @@
   qed
 qed
 
-lemma (in group) normal_inter_subgroup:
+lemma (in group) normal_Int_subgroup:
   assumes "subgroup H G"
     and "N \<lhd> G"
   shows "(N\<inter>H) \<lhd> (G\<lparr>carrier := H\<rparr>)"