diff -r 760e21900b01 -r 28e788ca2c5d src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Implementation/ML.thy	Thu Oct 22 21:16:49 2015 +0200
@@ -67,8 +67,8 @@
   reaching back to the earliest versions of the system by Larry
   Paulson.  See @{file "~~/src/Pure/thm.ML"}, for example.
 
-  The header includes at least @{verbatim Title} and @{verbatim
-  Author} entries, followed by a prose description of the purpose of
+  The header includes at least \<^verbatim>\<open>Title\<close> and \<^verbatim>\<open>Author\<close> entries,
+  followed by a prose description of the purpose of
   the module.  The latter can range from a single line to several
   paragraphs of explanations.
 
@@ -263,8 +263,8 @@
   explicit, if tactic combinators (tacticals) are used as usual.
 
   A tactic that requires a proof context needs to make that explicit as seen
-  in the @{verbatim ctxt} argument above. Do not refer to the background
-  theory of @{verbatim st} -- it is not a proper context, but merely a formal
+  in the \<^verbatim>\<open>ctxt\<close> argument above. Do not refer to the background
+  theory of \<^verbatim>\<open>st\<close> -- it is not a proper context, but merely a formal
   certificate.
 \<close>
 
@@ -516,8 +516,8 @@
 
   Object-logics like Isabelle/HOL are built within the Isabelle/ML/Isar
   environment by introducing suitable theories with associated ML modules,
-  either inlined within @{verbatim ".thy"} files, or as separate @{verbatim
-  ".ML"} files that are loading from some theory. Thus Isabelle/HOL is defined
+  either inlined within \<^verbatim>\<open>.thy\<close> files, or as separate \<^verbatim>\<open>.ML\<close> files that are
+  loading from some theory. Thus Isabelle/HOL is defined
   as a regular user-space application within the Isabelle framework. Further
   add-on tools can be implemented in ML within the Isar context in the same
   manner: ML is part of the standard repertoire of Isabelle, and there is no
@@ -970,8 +970,8 @@
 
   Depending on the user interface involved, these messages may appear
   in different text styles or colours.  The standard output for
-  batch sessions prefixes each line of warnings by @{verbatim
-  "###"} and errors by @{verbatim "***"}, but leaves anything else
+  batch sessions prefixes each line of warnings by \<^verbatim>\<open>###\<close> and errors by
+  \<^verbatim>\<open>***\<close>, but leaves anything else
   unchanged.  The message body may contain further markup and formatting,
   which is routinely used in the Prover IDE @{cite "isabelle-jedit"}.
 
@@ -1220,28 +1220,26 @@
   in itself a small string, which has either one of the following
   forms:
 
-  \<^enum> a single ASCII character ``\<open>c\<close>'', for example
-  ``@{verbatim a}'',
+  \<^enum> a single ASCII character ``\<open>c\<close>'', for example ``\<^verbatim>\<open>a\<close>'',
 
   \<^enum> a codepoint according to UTF-8 (non-ASCII byte sequence),
 
-  \<^enum> a regular symbol ``@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>ident\<close>@{verbatim ">"}'', for example ``@{verbatim "\<alpha>"}'',
-
-  \<^enum> a control symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^"}\<open>ident\<close>@{verbatim ">"}'', for example ``@{verbatim "\<^bold>"}'',
-
-  \<^enum> a raw symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^raw:"}\<open>text\<close>@{verbatim ">"}'' where \<open>text\<close> consists of printable characters
-  excluding ``@{verbatim "."}'' and ``@{verbatim ">"}'', for example
-  ``@{verbatim "\<^raw:$\sum_{i = 1}^n$>"}'',
-
-  \<^enum> a numbered raw control symbol ``@{verbatim \<open>\\<close>}@{verbatim
-  "<^raw"}\<open>n\<close>@{verbatim ">"}, where \<open>n\<close> consists of digits, for
-  example ``@{verbatim "\<^raw42>"}''.
+  \<^enum> a regular symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close>'', for example ``\<^verbatim>\<open>\<alpha>\<close>'',
+
+  \<^enum> a control symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close>'', for example ``\<^verbatim>\<open>\<^bold>\<close>'',
+
+  \<^enum> a raw symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw:\<close>\<open>text\<close>\<^verbatim>\<open>>\<close>'' where \<open>text\<close> consists of printable characters
+  excluding ``\<^verbatim>\<open>.\<close>'' and ``\<^verbatim>\<open>>\<close>'', for example
+  ``\<^verbatim>\<open>\<^raw:$\sum_{i = 1}^n$>\<close>'',
+
+  \<^enum> a numbered raw control symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw\<close>\<open>n\<close>\<^verbatim>\<open>>\<close>, where \<open>n\<close> consists
+  of digits, for example ``\<^verbatim>\<open>\<^raw42>\<close>''.
 
 
   The \<open>ident\<close> syntax for symbol names is \<open>letter
   (letter | digit)\<^sup>*\<close>, where \<open>letter = A..Za..z\<close> and \<open>digit = 0..9\<close>.  There are infinitely many regular symbols and
   control symbols, but a fixed collection of standard symbols is
-  treated specifically.  For example, ``@{verbatim "\<alpha>"}'' is
+  treated specifically.  For example, ``\<^verbatim>\<open>\<alpha>\<close>'' is
   classified as a letter, which means it may occur within regular
   Isabelle identifiers.
 
@@ -1255,9 +1253,9 @@
   \<^medskip>
   Output of Isabelle symbols depends on the print mode. For example,
   the standard {\LaTeX} setup of the Isabelle document preparation system
-  would present ``@{verbatim "\<alpha>"}'' as \<open>\<alpha>\<close>, and ``@{verbatim
-  "\<^bold>\<alpha>"}'' as \<open>\<^bold>\<alpha>\<close>. On-screen rendering usually works by mapping a
-  finite subset of Isabelle symbols to suitable Unicode characters.
+  would present ``\<^verbatim>\<open>\<alpha>\<close>'' as \<open>\<alpha>\<close>, and ``\<^verbatim>\<open>\<^bold>\<alpha>\<close>'' as \<open>\<^bold>\<alpha>\<close>. On-screen rendering
+  usually works by mapping a finite subset of Isabelle symbols to suitable
+  Unicode characters.
 \<close>
 
 text %mlref \<open>
@@ -1361,7 +1359,7 @@
     with @{ML YXML.parse_body} as key operation.
 
   Note that Isabelle/ML string literals may refer Isabelle symbols like
-  ``@{verbatim \<alpha>}'' natively, \<^emph>\<open>without\<close> escaping the backslash. This is a
+  ``\<^verbatim>\<open>\<alpha>\<close>'' natively, \<^emph>\<open>without\<close> escaping the backslash. This is a
   consequence of Isabelle treating all source text as strings of symbols,
   instead of raw characters.
 \<close>
@@ -1382,7 +1380,7 @@
   variations of encodings like UTF-8 or UTF-16 pose delicate questions
   about the multi-byte representations of its codepoint, which is outside
   of the 16-bit address space of the original Unicode standard from
-  the 1990-ies.  In Isabelle/ML it is just ``@{verbatim \<A>}''
+  the 1990-ies.  In Isabelle/ML it is just ``\<^verbatim>\<open>\<A>\<close>''
   literally, using plain ASCII characters beyond any doubts.\<close>
 
 
@@ -1541,13 +1539,13 @@
   Isabelle/ML, following standard conventions for their names and
   types.
 
-  Note that a function called @{verbatim lookup} is obliged to express its
+  Note that a function called \<^verbatim>\<open>lookup\<close> is obliged to express its
   partiality via an explicit option element.  There is no choice to
   raise an exception, without changing the name to something like
   \<open>the_element\<close> or \<open>get\<close>.
 
   The \<open>defined\<close> operation is essentially a contraction of @{ML
-  is_some} and @{verbatim "lookup"}, but this is sufficiently frequent to
+  is_some} and \<^verbatim>\<open>lookup\<close>, but this is sufficiently frequent to
   justify its independent existence.  This also gives the
   implementation some opportunity for peep-hole optimization.
 
@@ -1842,9 +1840,9 @@
 
   \<^medskip>
   An \<^emph>\<open>unevaluated expression\<close> is represented either as
-  unit abstraction @{verbatim "fn () => a"} of type
-  @{verbatim "unit -> 'a"} or as regular function
-  @{verbatim "fn a => b"} of type @{verbatim "'a -> 'b"}.  Both forms
+  unit abstraction \<^verbatim>\<open>fn () => a\<close> of type
+  \<^verbatim>\<open>unit -> 'a\<close> or as regular function
+  \<^verbatim>\<open>fn a => b\<close> of type \<^verbatim>\<open>'a -> 'b\<close>.  Both forms
   occur routinely, and special care is required to tell them apart ---
   the static type-system of SML is only of limited help here.
 
@@ -1908,7 +1906,7 @@
   all results are regular values, that list is returned.  Otherwise,
   the collection of all exceptions is raised, wrapped-up as collective
   parallel exception.  Note that the latter prevents access to
-  individual exceptions by conventional @{verbatim "handle"} of ML.
+  individual exceptions by conventional \<^verbatim>\<open>handle\<close> of ML.
 
   \<^descr> @{ML Par_Exn.release_first} is similar to @{ML
   Par_Exn.release_all}, but only the first (meaningful) exception that has
@@ -2010,8 +2008,7 @@
   @{index_ML Lazy.force: "'a lazy -> 'a"} \\
   \end{mldecls}
 
-  \<^descr> Type @{ML_type "'a lazy"} represents lazy values over type @{verbatim
-  "'a"}.
+  \<^descr> Type @{ML_type "'a lazy"} represents lazy values over type \<^verbatim>\<open>'a\<close>.
 
   \<^descr> @{ML Lazy.lazy}~\<open>(fn () => e)\<close> wraps the unevaluated
   expression \<open>e\<close> as unfinished lazy value.
@@ -2099,8 +2096,7 @@
   @{index_ML Future.fulfill: "'a future -> 'a -> unit"} \\
   \end{mldecls}
 
-  \<^descr> Type @{ML_type "'a future"} represents future values over type
-  @{verbatim "'a"}.
+  \<^descr> Type @{ML_type "'a future"} represents future values over type \<^verbatim>\<open>'a\<close>.
 
   \<^descr> @{ML Future.fork}~\<open>(fn () => e)\<close> registers the unevaluated
   expression \<open>e\<close> as unfinished future value, to be evaluated eventually