diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -100,7 +100,7 @@
   particular print mode features. For example, @{command
   "print_state"}~\<open>(latex)\<close> prints the current proof state with mathematical
   symbols and special characters represented in {\LaTeX} source, according to
-  the Isabelle style @{cite "isabelle-system"}.
+  the Isabelle style \<^cite>\<open>"isabelle-system"\<close>.
 
   Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more systematic
   way to include formal items into the printed text document.
@@ -273,7 +273,7 @@
   to abstract syntax, and the pretty printing. Special case annotations
   provide a simple means of specifying infix operators and binders.
 
-  Isabelle mixfix syntax is inspired by {\OBJ} @{cite OBJ}. It allows to
+  Isabelle mixfix syntax is inspired by {\OBJ} \<^cite>\<open>OBJ\<close>. It allows to
   specify any context-free priority grammar, which is more general than the
   fixity declarations of ML and Prolog.
 
@@ -411,7 +411,7 @@
 
   \<^medskip>
   Note that the general idea of pretty printing with blocks and breaks is
-  described in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
+  described in \<^cite>\<open>"paulson-ml2"\<close>; it goes back to \<^cite>\<open>"Oppen:1980"\<close>.
 \<close>
 
 
@@ -452,7 +452,7 @@
 text \<open>
   A \<^emph>\<open>binder\<close> is a variable-binding construct such as a quantifier. The idea
   to formalize \<open>\<forall>x. b\<close> as \<open>All (\<lambda>x. b)\<close> for \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close>
-  already goes back to @{cite church40}. Isabelle declarations of certain
+  already goes back to \<^cite>\<open>church40\<close>. Isabelle declarations of certain
   higher-order operators may be annotated with @{keyword_def "binder"}
   annotations as follows:
 
@@ -955,8 +955,7 @@
   carefully by syntax transformations.
 
   Pre-terms are further processed by the so-called \<^emph>\<open>check\<close> and \<^emph>\<open>uncheck\<close>
-  phases that are intertwined with type-inference (see also @{cite
-  "isabelle-implementation"}). The latter allows to operate on higher-order
+  phases that are intertwined with type-inference (see also \<^cite>\<open>"isabelle-implementation"\<close>). The latter allows to operate on higher-order
   abstract syntax with proper binding and type information already available.
 
   As a rule of thumb, anything that manipulates bindings of variables or