--- a/src/HOL/Proofs/Extraction/Higman.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Extraction/Higman.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -11,7 +11,7 @@
 
 text \<open>
   Formalization by Stefan Berghofer and Monika Seisenberger,
-  based on Coquand and Fridlender @{cite Coquand93}.
+  based on Coquand and Fridlender \<^cite>\<open>Coquand93\<close>.
 \<close>
 
 datatype letter = A | B