diff -r 35d8132633c6 -r ebaed09ce06e src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Sat May 22 21:52:13 2021 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Sat May 22 22:58:10 2021 +0200
@@ -626,7 +626,7 @@
   Structural composition ``\<open>m\<^sub>1\<close>\<^verbatim>\<open>;\<close>~\<open>m\<^sub>2\<close>'' means that method \<open>m\<^sub>1\<close> is
   applied with restriction to the first subgoal, then \<open>m\<^sub>2\<close> is applied
   consecutively with restriction to each subgoal that has newly emerged due to
-  \<open>m\<^sub>1\<close>. This is analogous to the tactic combinator \<^ML_op>\<open>THEN_ALL_NEW\<close> in
+  \<open>m\<^sub>1\<close>. This is analogous to the tactic combinator \<^ML_infix>\<open>THEN_ALL_NEW\<close> in
   Isabelle/ML, see also @{cite "isabelle-implementation"}. For example, \<open>(rule
   r; blast)\<close> applies rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>.