--- a/src/Doc/Logics_ZF/ZF_Isar.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Logics_ZF/ZF_Isar.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -93,7 +93,7 @@
     hints: @{syntax (ZF) "monos"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
   \<close>
 
-  See @{cite "isabelle-ZF"} for further information on inductive
+  See \<^cite>\<open>"isabelle-ZF"\<close> for further information on inductive
   definitions in ZF, but note that this covers the old-style theory
   format.
 \<close>