src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Wed Feb 01 20:07:13 2023 +0100
+++ b/src/HOL/Wellfounded.thy	Wed Feb 01 20:21:33 2023 +0100
@@ -617,7 +617,7 @@
 
 text \<open>
   Inductive definition of the accessible part \<open>acc r\<close> of a
-  relation; see also @{cite "paulin-tlca"}.
+  relation; see also \<^cite>\<open>"paulin-tlca"\<close>.
 \<close>
 
 inductive_set acc :: "('a \<times> 'a) set \<Rightarrow> 'a set" for r :: "('a \<times> 'a) set"