diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -214,7 +214,7 @@
 
 text \<open>
   Could be generalized to
-    @{prop "enumerate' S n = (SOME t. t \<in> s \<and> finite {s\<in>S. s < t} \<and> card {s\<in>S. s < t} = n)"}.
+    \<^prop>\<open>enumerate' S n = (SOME t. t \<in> s \<and> finite {s\<in>S. s < t} \<and> card {s\<in>S. s < t} = n)\<close>.
 \<close>
 
 primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"