src/Doc/Implementation/ML.thy

   @@{ML_antiquotation print} @{syntax name}?
   \<close>}
 
   \begin{description}
 
-  \item @{text "@{make_string}"} inlines a function to print arbitrary
-  values similar to the ML toplevel.  The result is compiler dependent
-  and may fall back on "?" in certain situations.
+  \item @{text "@{make_string}"} inlines a function to print arbitrary values
+  similar to the ML toplevel. The result is compiler dependent and may fall
+  back on "?" in certain situations. The value of configuration option
+  @{attribute_ref ML_print_depth} is used implicitly at compile-time.
 
   \item @{text "@{print f}"} uses the ML function @{text "f: string ->
   unit"} to output the result of @{text "@{make_string}"} above,
   together with the source position of the antiquotation.  The default
   output function is @{ML writeln}.