diff -r 4c3bb14f5c2b -r 13b10ca71150 src/HOL/Algebra/Indexed_Polynomials.thy
--- a/src/HOL/Algebra/Indexed_Polynomials.thy	Sat Apr 13 19:27:37 2019 +0100
+++ b/src/HOL/Algebra/Indexed_Polynomials.thy	Sun Apr 14 11:59:54 2019 +0100
@@ -336,7 +336,7 @@
 qed
 
 
-subsection \<open>Link with Weak_Morphisms\<close>
+subsection \<open>Link with Weak Morphisms\<close>
 
 text \<open>We study some elements of the contradiction needed in the algebraic closure existence proof. \<close>