--- 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>