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