--- a/ProgTutorial/Advanced.thy	Thu Nov 17 12:20:19 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Thu Nov 17 16:33:49 2011 +0000
@@ -165,7 +165,8 @@
   val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy
   val trm1 = Syntax.read_term_global tmp_thy' "FOO baz"
   val trm2 = Syntax.read_term_global thy "FOO baz"
-  val _ = writeln (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2)
+  val _ = pwriteln 
+    (Pretty.str (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2))
 in
   thy
 end *}
@@ -192,6 +193,11 @@
   inference. This is relevant in situations where definitions are made later, 
   but parsing and type inference has to take already proceed as if the definitions 
   were already made.
+
+  \begin{readmore}
+  Most of the functions about theories are implemented in
+  @{ML_file "Pure/theory.ML"} and @{ML_file "Pure/global_theory.ML"}.
+  \end{readmore}
 *}
 
 section {* Contexts *}
@@ -315,7 +321,7 @@
   "([\"y\", \"ya\", \"z\"], ...)"}
 
   Now a fresh variant for the second occurence of @{text y} is created
-  avoiding any clash. In this way we can also create free variables
+  avoiding any clash. In this way we can also create fresh free variables
   that avoid any clashes with fixed variables. In Line~3 below we fix
   the variable @{text x} in the context @{text ctxt1}. Next we want to
   create two fresh variables of type @{typ nat} as variants of the
@@ -459,10 +465,11 @@
 end"
   "?P ?x ?y ?z ?x ?y ?z"}
 
-  Since we fixed all variables in @{text ctxt1}, in the result all of them 
-  are schematic. The great point of contexts is that exporting from one to 
-  another is not just concerned with variables, but also assumptions. For this we
-  can use the function @{ML_ind export in Assumption} from the structure
+  Since we fixed all variables in @{text ctxt1}, in the exported
+  result all of them are schematic. The great point of contexts is
+  that exporting from one to another is not just restricted to
+  variables, but also works with assumptions. For this we can use the
+  function @{ML_ind export in Assumption} from the structure
   @{ML_struct Assumption}. Consider the following code.
 
   @{ML_response_fake [display, gray, linenos]
@@ -552,7 +559,7 @@
 oops
 *)
 
-section {* Local Theories (TBD) *}
+section {* Local Theories and Local Setups\label{sec:local} (TBD) *}
 
 text {*
   In contrast to an ordinary theory, which simply consists of a type