--- a/ProgTutorial/General.thy	Mon Nov 09 09:25:51 2009 +0100
+++ b/ProgTutorial/General.thy	Mon Nov 09 09:48:38 2009 +0100
@@ -694,13 +694,13 @@
   @{ML_type "Type.tyenv"}, which maps schematic type variables to types (and
   sorts). Below we use the function @{ML_ind typ_unify in Sign} from the 
   structure @{ML_struct Sign} for unifying
-  the types @{text "?'a * nat"} and @{text "?'b list * ?'b"}. This will
+  the types @{text "?'a * ?'b"} and @{text "?'b list * nat"}. This will
   produce the mapping @{text "[?'a := ?'b list, ?'b := nat]"}.
 *}
 
 ML{*val (tyenv_unif, _) = let
-  val ty1 = @{typ_pat "?'a * nat"}
-  val ty2 = @{typ_pat "?'b list * ?'b"}
+  val ty1 = @{typ_pat "?'a * ?'b"}
+  val ty2 = @{typ_pat "?'b list * nat"}
 in
   Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) 
 end*}
@@ -709,8 +709,8 @@
   The value @{ML_ind empty in Vartab} stands for the empty type environment, 
   which is the value for starting the unification without any 
   instantiations.\footnote{\bf FIXME: what is 0?} 
-  We can print out the resulting 
-  type environment with the built-in function @{ML_ind dest in Vartab}.
+  We can print out the resulting type environment @{ML tyenv_unif} 
+  with the built-in function @{ML_ind dest in Vartab}.
 
   @{ML_response_fake [display,gray]
   "Vartab.dest tyenv_unif"
@@ -785,8 +785,8 @@
   "bool list * nat"}
 
   Be careful to observe the difference: use @{ML subst_type in Envir} 
-  for matchers and @{ML norm_type in Envir} for unifiers. To show the 
-  difference let us calculate the following matcher.
+  for matchers and @{ML norm_type in Envir} for unifiers. To make the 
+  difference explicit let us calculate the following matcher.
 *}
 
 ML{*val tyenv_match' = let
@@ -798,15 +798,16 @@
 
 text {*
   Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. Consider
-  again the type @{text "?'a * ?'b"}. If we apply 
-  @{ML norm_type in Envir} to the matcher we obtain
+  again the type @{text "?'a * ?'b"}, which we used in the unification
+  and matching problems. If we apply @{ML norm_type in Envir} to 
+  the matcher we obtain
 
   @{ML_response_fake [display, gray]
   "Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}"
   "nat list * nat"}
 
   which is not a matcher for the second matching problem, and if
-  we apply @{ML subst_type in Envir} to the unifier
+  we apply @{ML subst_type in Envir} to the unifier we obtain
 
   @{ML_response_fake [display, gray]
   "Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
@@ -819,9 +820,9 @@
   in @{ML_file "Pure/type.ML"}. The ``interface'' functions for them
   are in @{ML_file "Pure/sign.ML"}. Matching and unification produce type environments
   as results. These are implemented in @{ML_file "Pure/envir.ML"}.
-  This file also includes the substitution and normalisation functions. 
-  Environments are lookup tables that are implemented in 
-  @{ML_file "Pure/term_ord.ML"}.
+  This file also includes the substitution and normalisation functions,
+  that apply a type environment to a type. Type environments are lookup 
+  tables which are implemented in @{ML_file "Pure/term_ord.ML"}.
   \end{readmore}
 *}