diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Groups_List.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -252,7 +252,7 @@
   "sum_list (map f [k..l]) = sum f (set [k..l])"
   by (simp add: sum_list_distinct_conv_sum_set)
 
-text \<open>General equivalence between @{const sum_list} and @{const sum}\<close>
+text \<open>General equivalence between \<^const>\<open>sum_list\<close> and \<^const>\<open>sum\<close>\<close>
 lemma (in monoid_add) sum_list_sum_nth:
   "sum_list xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
   using interv_sum_list_conv_sum_set_nat [of "(!) xs" 0 "length xs"] by (simp add: map_nth)
@@ -327,7 +327,7 @@
 qed
 
 
-subsection \<open>Further facts about @{const List.n_lists}\<close>
+subsection \<open>Further facts about \<^const>\<open>List.n_lists\<close>\<close>
 
 lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
   by (induct n) (auto simp add: comp_def length_concat sum_list_triv)