src/Doc/Implementation/ML.thy

--- a/src/Doc/Implementation/ML.thy	Wed Dec 06 14:19:36 2017 +0100
+++ b/src/Doc/Implementation/ML.thy	Wed Dec 06 15:46:35 2017 +0100
@@ -695,7 +695,7 @@
   @{rail \<open>
   @@{ML_antiquotation make_string}
   ;
-  @@{ML_antiquotation print} @{syntax name}?
+  @@{ML_antiquotation print} embedded?
   \<close>}
 
   \<^descr> \<open>@{make_string}\<close> inlines a function to print arbitrary values similar to