--- a/ProgTutorial/General.thy	Tue Nov 10 04:57:42 2009 +0100
+++ b/ProgTutorial/General.thy	Tue Nov 10 06:24:00 2009 +0100
@@ -689,7 +689,7 @@
   Section~\ref{sec:antiquote} in order to construct examples involving
   schematic variables.
 
-  Let us begin with describing the unification and the matching function for
+  Let us begin with describing the unification and matching function for
   types.  Both return type environments, ML-type @{ML_type "Type.tyenv"},
   which map schematic type variables to types (and sorts). Below we use the
   function @{ML_ind typ_unify in Sign} from the structure @{ML_struct Sign}
@@ -698,7 +698,7 @@
   ?'b list, ?'b := nat]"}.
 *}
 
-ML{*val (tyenv_unif, _) = let
+ML %linenosgray{*val (tyenv_unif, _) = let
   val ty1 = @{typ_pat "?'a * ?'b"}
   val ty2 = @{typ_pat "?'b list * nat"}
 in
@@ -706,9 +706,9 @@
 end*}
 
 text {* 
-  The environment @{ML_ind "Vartab.empty"} stands for the empty type environment, 
-  which is needed for starting the unification without any 
-  (pre)instantiations.  In case of a failure 
+  The environment @{ML_ind "Vartab.empty"} in line 5 stands for the 
+  empty type environment, which is needed for starting the unification 
+  without any (pre)instantiations.  In case of a failure 
   @{ML typ_unify in Sign} will throw the exception @{text TUNIFY}.
   We can print out the resulting type environment @{ML tyenv_unif} 
   with the built-in function @{ML_ind dest in Vartab} from the structure
@@ -749,22 +749,25 @@
 
 text {*
   The first components in this list stand for the schematic type variables and
-  the second are the associated sorts and types. In what follows we will use
-  the pretty-printing function in Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s.
-  For the type environment from the example this function prints out the 
-  more legible: 
+  the second are the associated sorts and types. In this example the sort
+  is the default sort @{text "HOL.type"}. We will use in what follows
+  the pretty-printing function from Figure~\ref{fig:prettyenv} for 
+  @{ML_type "Type.tyenv"}s. For the type environment in the example 
+  this function prints out the more legible: 
 
   @{ML_response_fake [display, gray]
   "pretty_tyenv @{context} tyenv_unif"
   "[?'a := ?'b list, ?'b := nat]"}
 
-  The index @{text 0} in the example above is the maximal index of the schematic 
-  type variables occuring in @{text ty1} and @{text ty2}. It will be increased
-  whenever a new schematic type variable is introduced during unification.
-  This is for example the case when two schematic type variables have different, 
-  incomparable sorts. Then a new schematic type variable is introduced with 
-  the combined sorts. To show this let us use two sorts, @{text "s1"} and @{text "s2"}, 
-  which we attach to the schematic type variables @{text "?'a"} and @{text "?'b"}. 
+  The index @{text 0} in Line 5 in the example above is the maximal index of
+  the schematic type variables occuring in @{text ty1} and @{text ty2}. This
+  index will be increased whenever a new schematic type variable is introduced
+  during unification.  This is for example the case when two schematic type
+  variables have different, incomparable sorts. Then a new schematic type
+  variable is introduced with the combined sorts. To show this let us assume two
+  sorts, say @{text "s1"} and @{text "s2"}, which we attach to the schematic type
+  variables @{text "?'a"} and @{text "?'b"}. Since we do not make any assumption
+  about the sors, they are incomparable, leading to the type environment:
 *}
 
 ML{*val (tyenv, index) = let
@@ -775,8 +778,8 @@
 end*}
 
 text {*
-  To print out the calculated type environment we also switch on the printing 
-  of sort information.
+  To print out this type environment we switch on the printing of sort 
+  information.
 *}
 
 ML{*show_sorts := true*}
@@ -801,7 +804,7 @@
 text {*
   The way the unification function @{ML typ_unify in Sign} is implemented 
   using an initial type environment and initial index makes it easy to
-  unifying of more than two terms. For example 
+  unify more than two terms. For example 
 *}
 
 ML{*val (tyenvs, _) = let
@@ -812,7 +815,8 @@
 end*}
 
 text {*
-  Let us now return again to the unifier from the first example.
+  Let us now return again to the unifier from the first example in this
+  section.
 
   @{ML_response_fake [display, gray]
   "pretty_tyenv @{context} tyenv_unif"
@@ -824,7 +828,6 @@
   instantiation for @{text "?'a"}.  In unification theory, this is often
   called an instantiation in \emph{triangular form}. These not fully solved 
   instantiations are used because of performance reasons.
-
   To apply a type environment in triangular form to a type, say @{text "?'a *
   ?'b"}, you should use the function @{ML_ind norm_type in Envir}:
 
@@ -1437,7 +1440,7 @@
   \end{readmore}
 
   The simplifier can be used to unfold definition in theorems. To show
-  this we build the theorem @{term "True \<equiv> True"} (Line 1) and then 
+  this, we build the theorem @{term "True \<equiv> True"} (Line 1) and then 
   unfold the constant @{term "True"} according to its definition (Line 2).
 
   @{ML_response_fake [display,gray,linenos]