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
+  imports Main
 begin
 
 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>
 
 
 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>
 
 
 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>
 
 
 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>
 
 
 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>
 
 
 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>
 
 
 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/Seq.thy b/src/HOL/Examples/Seq.thy
--- a/src/HOL/Examples/Seq.thy
+++ b/src/HOL/Examples/Seq.thy
@@ -1,35 +1,35 @@
 (*  Title:      HOL/Examples/Seq.thy
     Author:     Makarius
 *)
 
 section \<open>Finite sequences\<close>
 
 theory Seq
-imports Main
+  imports Main
 begin
 
 datatype 'a seq = Empty | Seq 'a "'a seq"
 
 fun conc :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq"
 where
   "conc Empty ys = ys"
 | "conc (Seq x xs) ys = Seq x (conc xs ys)"
 
 fun reverse :: "'a seq \<Rightarrow> 'a seq"
 where
   "reverse Empty = Empty"
 | "reverse (Seq x xs) = conc (reverse xs) (Seq x Empty)"
 
 lemma conc_empty: "conc xs Empty = xs"
   by (induct xs) simp_all
 
 lemma conc_assoc: "conc (conc xs ys) zs = conc xs (conc ys zs)"
   by (induct xs) simp_all
 
 lemma reverse_conc: "reverse (conc xs ys) = conc (reverse ys) (reverse xs)"
   by (induct xs) (simp_all add: conc_empty conc_assoc)
 
 lemma reverse_reverse: "reverse (reverse xs) = xs"
   by (induct xs) (simp_all add: reverse_conc)
 
 end
diff --git a/src/Tools/SML/Examples.thy b/src/Tools/SML/Examples.thy
--- a/src/Tools/SML/Examples.thy
+++ b/src/Tools/SML/Examples.thy
@@ -1,52 +1,52 @@
 (*  Title:      Tools/SML/Examples.thy
     Author:     Makarius
 *)
 
 section \<open>Standard ML within the Isabelle environment\<close>
 
 theory Examples
-imports Pure
+  imports Pure
 begin
 
 text \<open>
   Isabelle/ML is a somewhat augmented version of Standard ML, with various
   add-ons that are indispensable for Isabelle development, but may cause
   conflicts with independent projects in plain Standard ML.
 
   The Isabelle/Isar command \<^theory_text>\<open>SML_file\<close> supports official Standard ML within
   the Isabelle environment, with full support in the Prover IDE
   (Isabelle/jEdit).
 
   Here is a very basic example that defines the factorial function and
   evaluates it for some arguments.
 \<close>
 
 SML_file \<open>factorial.sml\<close>
 
 text \<open>
   The subsequent example illustrates the use of multiple \<^theory_text>\<open>SML_file\<close> commands
   to build larger Standard ML projects. The toplevel SML environment is
   enriched cumulatively within the theory context of Isabelle ---
   independently of the Isabelle/ML environment.
 \<close>
 
 SML_file \<open>Example.sig\<close>
 SML_file \<open>Example.sml\<close>
 
 
 text \<open>
   Isabelle/ML and SML share a common run-time system, but the static
   environments are separate. It is possible to exchange toplevel bindings via
   separate commands like this.
 \<close>
 
 SML_export \<open>val f = factorial\<close>  \<comment> \<open>re-use factorial from SML environment\<close>
 ML \<open>f 42\<close>
 
 SML_import \<open>val println = Output.writeln\<close>
   \<comment> \<open>re-use Isabelle/ML channel for SML\<close>
 
 SML_import \<open>val par_map = Par_List.map\<close>
   \<comment> \<open>re-use Isabelle/ML parallel list combinator for SML\<close>
 
 end