diff -r 35d8132633c6 -r ebaed09ce06e src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Sat May 22 21:52:13 2021 +0200
+++ b/src/Doc/Implementation/ML.thy	Sat May 22 22:58:10 2021 +0200
@@ -1608,7 +1608,7 @@
 
   The unwieldy name of \<^ML>\<open>Unsynchronized.ref\<close> for the constructor for
   references in Isabelle/ML emphasizes the inconveniences caused by
-  mutability. Existing operations \<^ML>\<open>!\<close> and \<^ML_op>\<open>:=\<close> are unchanged,
+  mutability. Existing operations \<^ML>\<open>!\<close> and \<^ML_infix>\<open>:=\<close> are unchanged,
   but should be used with special precautions, say in a strictly local
   situation that is guaranteed to be restricted to sequential evaluation ---
   now and in the future.