tuned;

--- a/src/Doc/IsarImplementation/Logic.thy	Sun Aug 18 13:58:33 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy	Sun Aug 18 15:10:18 2013 +0200
@@ -881,8 +881,7 @@
   The @{text "TYPE"} constructor is the canonical representative of
   the unspecified type @{text "\<alpha> itself"}; it essentially injects the
   language of types into that of terms.  There is specific notation
-  @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>
- itself\<^esub>"}.
+  @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau> itself\<^esub>"}.
   Although being devoid of any particular meaning, the term @{text
   "TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term
   language.  In particular, @{text "TYPE(\<alpha>)"} may be used as formal

--- a/src/Doc/IsarImplementation/ML.thy	Sun Aug 18 13:58:33 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Sun Aug 18 15:10:18 2013 +0200
@@ -800,7 +800,7 @@
   reasoning.}
 
   Currying gives some flexiblity due to \emph{partial application}.  A
-  function @{text "f: \<tau>\<^sub>1 \<rightarrow> \<tau>\<^bsub>2\<^esub> \<rightarrow> \<tau>"} can be applied to @{text "x: \<tau>\<^sub>1"}
+  function @{text "f: \<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2 \<rightarrow> \<tau>"} can be applied to @{text "x: \<tau>\<^sub>1"}
   and the remaining @{text "(f x): \<tau>\<^sub>2 \<rightarrow> \<tau>"} passed to another function
   etc.  How well this works in practice depends on the order of
   arguments.  In the worst case, arguments are arranged erratically,
@@ -904,8 +904,8 @@
   parametrized by arguments of type @{text "\<alpha>"}.  Given @{text "a: \<alpha>"}
   the partial application @{text "(f a): \<beta> \<rightarrow> \<beta>"} operates
   homogeneously on @{text "\<beta>"}.  This can be iterated naturally over a
-  list of parameters @{text "[a\<^sub>1, \<dots>, a\<^sub>n]"} as @{text "f a\<^sub>1 #> \<dots> #> f
-  a\<^bsub>n\<^esub>\<^bsub>\<^esub>"}.  The latter expression is again a function @{text "\<beta> \<rightarrow> \<beta>"}.
+  list of parameters @{text "[a\<^sub>1, \<dots>, a\<^sub>n]"} as @{text "f a\<^sub>1 #> \<dots> #> f a\<^sub>n"}.
+  The latter expression is again a function @{text "\<beta> \<rightarrow> \<beta>"}.
   It can be applied to an initial configuration @{text "b: \<beta>"} to
   start the iteration over the given list of arguments: each @{text
   "a"} in @{text "a\<^sub>1, \<dots>, a\<^sub>n"} is applied consecutively by updating a