diff -r c8a2755bf220 -r ff784d5a5bfb src/Doc/Implementation/Eq.thy
--- a/src/Doc/Implementation/Eq.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/Doc/Implementation/Eq.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -43,12 +43,12 @@
   same reasoning schemes as theorems that can be composed like object-level
   rules as explained in \secref{sec:obj-rules}.
 
-  For example, @{ML Thm.symmetric} as Pure inference is an ML function that
+  For example, \<^ML>\<open>Thm.symmetric\<close> as Pure inference is an ML function that
   maps a theorem \<open>th\<close> stating \<open>t \<equiv> u\<close> to one stating \<open>u \<equiv> t\<close>. In contrast,
   @{thm [source] Pure.symmetric} as Pure theorem expresses the same reasoning
   in declarative form. If used like \<open>th [THEN Pure.symmetric]\<close> in Isar source
   notation, it achieves a similar effect as the ML inference function,
-  although the rule attribute @{attribute THEN} or ML operator @{ML "op RS"}
+  although the rule attribute @{attribute THEN} or ML operator \<^ML>\<open>op RS\<close>
   involve the full machinery of higher-order unification (modulo
   \<open>\<beta>\<eta>\<close>-conversion) and lifting of \<open>\<And>/\<Longrightarrow>\<close> contexts.
 \<close>
@@ -99,21 +99,21 @@
   @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
   \end{mldecls}
 
-  \<^descr> @{ML rewrite_rule}~\<open>ctxt rules thm\<close> rewrites the whole theorem by the
+  \<^descr> \<^ML>\<open>rewrite_rule\<close>~\<open>ctxt rules thm\<close> rewrites the whole theorem by the
   given rules.
 
-  \<^descr> @{ML rewrite_goals_rule}~\<open>ctxt rules thm\<close> rewrites the outer premises of
+  \<^descr> \<^ML>\<open>rewrite_goals_rule\<close>~\<open>ctxt rules thm\<close> rewrites the outer premises of
   the given theorem. Interpreting the same as a goal state
   (\secref{sec:tactical-goals}) it means to rewrite all subgoals (in the same
-  manner as @{ML rewrite_goals_tac}).
+  manner as \<^ML>\<open>rewrite_goals_tac\<close>).
 
-  \<^descr> @{ML rewrite_goal_tac}~\<open>ctxt rules i\<close> rewrites subgoal \<open>i\<close> by the given
+  \<^descr> \<^ML>\<open>rewrite_goal_tac\<close>~\<open>ctxt rules i\<close> rewrites subgoal \<open>i\<close> by the given
   rewrite rules.
 
-  \<^descr> @{ML rewrite_goals_tac}~\<open>ctxt rules\<close> rewrites all subgoals by the given
+  \<^descr> \<^ML>\<open>rewrite_goals_tac\<close>~\<open>ctxt rules\<close> rewrites all subgoals by the given
   rewrite rules.
 
-  \<^descr> @{ML fold_goals_tac}~\<open>ctxt rules\<close> essentially uses @{ML rewrite_goals_tac}
+  \<^descr> \<^ML>\<open>fold_goals_tac\<close>~\<open>ctxt rules\<close> essentially uses \<^ML>\<open>rewrite_goals_tac\<close>
   with the symmetric form of each member of \<open>rules\<close>, re-ordered to fold longer
   expression first. This supports to idea to fold primitive definitions that
   appear in expended form in the proof state.