diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Algebra/Embedded_Algebras.thy
--- a/src/HOL/Algebra/Embedded_Algebras.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Algebra/Embedded_Algebras.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -361,7 +361,7 @@
   using Span_eq_combine_set_length_version[OF assms] by blast
 
 
-subsection \<open>Span as the minimal subgroup that contains @{term"K <#> (set Us)"}\<close>
+subsection \<open>Span as the minimal subgroup that contains \<^term>\<open>K <#> (set Us)\<close>\<close>
 
 text \<open>Now we show the link between Span and Group.generate\<close>