diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Codegen/Inductive_Predicate.thy
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
   which turns inductive specifications into equational ones, from
   which in turn executable code can be generated.  The mechanisms of
   this compiler are described in detail in
-  @{cite "Berghofer-Bulwahn-Haftmann:2009:TPHOL"}.
+  \<^cite>\<open>"Berghofer-Bulwahn-Haftmann:2009:TPHOL"\<close>.
 
   Consider the simple predicate \<^const>\<open>append\<close> given by these two
   introduction rules: