diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/ex/Erdoes_Szekeres.thy
--- a/src/HOL/ex/Erdoes_Szekeres.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/ex/Erdoes_Szekeres.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -8,7 +8,7 @@
 imports Main
 begin
 
-subsection \<open>Addition to @{theory HOL.Lattices_Big} Theory\<close>
+subsection \<open>Addition to \<^theory>\<open>HOL.Lattices_Big\<close> Theory\<close>
 
 lemma Max_gr:
   assumes "finite A"
@@ -16,7 +16,7 @@
   shows "x < Max A"
 using assms Max_ge less_le_trans by blast
 
-subsection \<open>Additions to @{theory HOL.Finite_Set} Theory\<close>
+subsection \<open>Additions to \<^theory>\<open>HOL.Finite_Set\<close> Theory\<close>
 
 lemma obtain_subset_with_card_n:
   assumes "n \<le> card S"