doc-src/IsarImplementation/Thy/document/Prelim.tex

   \indexdef{}{ML}{Binding.empty}\verb|Binding.empty: binding| \\
   \indexdef{}{ML}{Binding.name}\verb|Binding.name: string -> binding| \\
   \indexdef{}{ML}{Binding.qualify}\verb|Binding.qualify: bool -> string -> binding -> binding| \\
   \indexdef{}{ML}{Binding.prefix}\verb|Binding.prefix: bool -> string -> binding -> binding| \\
   \indexdef{}{ML}{Binding.conceal}\verb|Binding.conceal: binding -> binding| \\
-  \indexdef{}{ML}{Binding.str\_of}\verb|Binding.str_of: binding -> string| \\
+  \indexdef{}{ML}{Binding.print}\verb|Binding.print: binding -> string| \\
   \end{mldecls}
   \begin{mldecls}
   \indexdef{}{ML type}{Name\_Space.naming}\verb|type Name_Space.naming| \\
   \indexdef{}{ML}{Name\_Space.default\_naming}\verb|Name_Space.default_naming: Name_Space.naming| \\
   \indexdef{}{ML}{Name\_Space.add\_path}\verb|Name_Space.add_path: string -> Name_Space.naming -> Name_Space.naming| \\

   binding shall refer to an entity that serves foundational purposes
   only.  This flag helps to mark implementation details of
   specification mechanism etc.  Other tools should not depend on the
   particulars of concealed entities (cf.\ \verb|Name_Space.is_concealed|).
 
-  \item \verb|Binding.str_of|~\isa{binding} produces a string
+  \item \verb|Binding.print|~\isa{binding} produces a string
   representation for human-readable output, together with some formal
   markup that might get used in GUI front-ends, for example.
 
   \item Type \verb|Name_Space.naming| represents the abstract
   concept of a naming policy.