diff -r bcea02893d17 -r 49318345c332 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Fri Sep 08 19:55:18 2017 +0200
+++ b/src/Doc/Implementation/ML.thy	Sat Sep 09 16:51:55 2017 +0200
@@ -946,9 +946,9 @@
   Another benefit of @{ML add_content} is its ``open'' form as a function on
   buffers that can be continued in further linear transformations, folding
   etc. Thus it is more compositional than the naive @{ML slow_content}. As
-  realistic example, compare the old-style @{ML "Term.maxidx_of_term: term ->
-  int"} with the newer @{ML "Term.maxidx_term: term -> int -> int"} in
-  Isabelle/Pure.
+  realistic example, compare the old-style
+  @{ML "Term.maxidx_of_term: term -> int"} with the newer @{ML
+  "Term.maxidx_term: term -> int -> int"} in Isabelle/Pure.
 
   Note that @{ML fast_content} above is only defined as example. In many
   practical situations, it is customary to provide the incremental @{ML
@@ -1851,18 +1851,18 @@
   evaluation via promises, evaluation with time limit etc.
 
   \<^medskip>
-  An \<^emph>\<open>unevaluated expression\<close> is represented either as 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
+  An \<^emph>\<open>unevaluated expression\<close> is represented either as 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.
 
-  The first form is more intuitive: some combinator \<open>(unit -> 'a) -> 'a\<close>
-  applies the given function to \<open>()\<close> to initiate the postponed evaluation
-  process. The second form is more flexible: some combinator \<open>('a -> 'b) -> 'a
-  -> 'b\<close> acts like a modified form of function application; several such
-  combinators may be cascaded to modify a given function, before it is
-  ultimately applied to some argument.
+  The first form is more intuitive: some combinator \<^verbatim>\<open>(unit -> 'a) -> 'a\<close>
+  applies the given function to \<^verbatim>\<open>()\<close> to initiate the postponed evaluation
+  process. The second form is more flexible: some combinator
+  \<^verbatim>\<open>('a -> 'b) -> 'a -> 'b\<close> acts like a modified form of function application;
+  several such combinators may be cascaded to modify a given function, before
+  it is ultimately applied to some argument.
 
   \<^medskip>
   \<^emph>\<open>Reified results\<close> make the disjoint sum of regular values versions