diff --git a/src/HOL/Examples/ML.thy b/src/HOL/Examples/ML.thy
--- a/src/HOL/Examples/ML.thy
+++ b/src/HOL/Examples/ML.thy
@@ -1,157 +1,157 @@
 (*  Title:      HOL/Examples/ML.thy
     Author:     Makarius
 *)
 
 section \<open>Isabelle/ML basics\<close>
 
 theory "ML"
 imports Main
 begin
 
-section \<open>ML expressions\<close>
+subsection \<open>ML expressions\<close>
 
 text \<open>
   The Isabelle command \<^theory_text>\<open>ML\<close> allows to embed Isabelle/ML source into the
   formal text. It is type-checked, compiled, and run within that environment.
 
   Note that side-effects should be avoided, unless the intention is to change
   global parameters of the run-time environment (rare).
 
   ML top-level bindings are managed within the theory context.
 \<close>
 
 ML \<open>1 + 1\<close>
 
 ML \<open>val a = 1\<close>
 ML \<open>val b = 1\<close>
 ML \<open>val c = a + b\<close>
 
 
-section \<open>Antiquotations\<close>
+subsection \<open>Antiquotations\<close>
 
 text \<open>
   There are some language extensions (via antiquotations), as explained in the
   ``Isabelle/Isar implementation manual'', chapter 0.
 \<close>
 
 ML \<open>length []\<close>
 ML \<open>\<^assert> (length [] = 0)\<close>
 
 
 text \<open>Formal entities from the surrounding context may be referenced as
   follows:\<close>
 
 term "1 + 1"   \<comment> \<open>term within theory source\<close>
 
 ML \<open>\<^term>\<open>1 + 1\<close>   (* term as symbolic ML datatype value *)\<close>
 
 ML \<open>\<^term>\<open>1 + (1::int)\<close>\<close>
 
 
 ML \<open>
   (* formal source with position information *)
   val s = \<open>1 + 1\<close>;
 
   (* read term via old-style string interface *)
   val t = Syntax.read_term \<^context> (Syntax.implode_input s);
 \<close>
 
 
-section \<open>Recursive ML evaluation\<close>
+subsection \<open>Recursive ML evaluation\<close>
 
 ML \<open>
   ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
   ML \<open>val b = @{thm sym}\<close>;
   val c = @{thm trans}
   val thms = [a, b, c];
 \<close>
 
 
-section \<open>IDE support\<close>
+subsection \<open>IDE support\<close>
 
 text \<open>
   ML embedded into the Isabelle environment is connected to the Prover IDE.
   Poly/ML provides:
 
     \<^item> precise positions for warnings / errors
     \<^item> markup for defining positions of identifiers
     \<^item> markup for inferred types of sub-expressions
     \<^item> pretty-printing of ML values with markup
     \<^item> completion of ML names
     \<^item> source-level debugger
 \<close>
 
 ML \<open>fn i => fn list => length list + i\<close>
 
 
-section \<open>Example: factorial and ackermann function in Isabelle/ML\<close>
+subsection \<open>Example: factorial and ackermann function in Isabelle/ML\<close>
 
 ML \<open>
   fun factorial 0 = 1
     | factorial n = n * factorial (n - 1)
 \<close>
 
 ML \<open>factorial 42\<close>
 ML \<open>factorial 10000 div factorial 9999\<close>
 
 text \<open>See \<^url>\<open>http://mathworld.wolfram.com/AckermannFunction.html\<close>.\<close>
 
 ML \<open>
   fun ackermann 0 n = n + 1
     | ackermann m 0 = ackermann (m - 1) 1
     | ackermann m n = ackermann (m - 1) (ackermann m (n - 1))
 \<close>
 
 ML \<open>timeit (fn () => ackermann 3 10)\<close>
 
 
-section \<open>Parallel Isabelle/ML\<close>
+subsection \<open>Parallel Isabelle/ML\<close>
 
 text \<open>
   Future.fork/join/cancel manage parallel evaluation.
 
   Note that within Isabelle theory documents, the top-level command boundary
   may not be transgressed without special precautions. This is normally
   managed by the system when performing parallel proof checking.
 \<close>
 
 ML \<open>
   val x = Future.fork (fn () => ackermann 3 10);
   val y = Future.fork (fn () => ackermann 3 10);
   val z = Future.join x + Future.join y
 \<close>
 
 text \<open>
   The \<^ML_structure>\<open>Par_List\<close> module provides high-level combinators for
   parallel list operations.
 \<close>
 
 ML \<open>timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\<close>
 ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close>
 
 
-section \<open>Function specifications in Isabelle/HOL\<close>
+subsection \<open>Function specifications in Isabelle/HOL\<close>
 
 fun factorial :: "nat \<Rightarrow> nat"
 where
   "factorial 0 = 1"
 | "factorial (Suc n) = Suc n * factorial n"
 
 term "factorial 4"  \<comment> \<open>symbolic term\<close>
 value "factorial 4"  \<comment> \<open>evaluation via ML code generation in the background\<close>
 
 declare [[ML_source_trace]]
 ML \<open>\<^term>\<open>factorial 4\<close>\<close>  \<comment> \<open>symbolic term in ML\<close>
 ML \<open>@{code "factorial"}\<close>  \<comment> \<open>ML code from function specification\<close>
 
 
 fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 where
   "ackermann 0 n = n + 1"
 | "ackermann (Suc m) 0 = ackermann m 1"
 | "ackermann (Suc m) (Suc n) = ackermann m (ackermann (Suc m) n)"
 
 value "ackermann 3 5"
 
 end
 
diff --git a/src/HOL/Examples/document/root.tex b/src/HOL/Examples/document/root.tex
--- a/src/HOL/Examples/document/root.tex
+++ b/src/HOL/Examples/document/root.tex
@@ -1,25 +1,27 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
 
 \isabellestyle{literal}
 \usepackage{pdfsetup}\urlstyle{rm}
 
 
 \hyphenation{Isabelle}
 
 \begin{document}
 
 \title{Notable Examples in Isabelle/HOL}
 \maketitle
 
+\tableofcontents
+
 \parindent 0pt \parskip 0.5ex
 
 \input{session}
 
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}