diff -r 76b1b679e845 -r 272ba2cceeb2 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Sat Nov 07 01:44:11 2009 +0100
+++ b/ProgTutorial/General.thy	Sat Nov 07 10:08:09 2009 +0100
@@ -185,7 +185,7 @@
   "@{typ \"bool\"}"
   "bool"}
 
-  the pretty printed version of @{text "bool"}. However, in PolyML it is 
+  that is the pretty printed version of @{text "bool"}. However, in PolyML it is 
   easy to install your own pretty printer. With the function below we 
   mimic the behaviour of the usual pretty printer for 
   datatypes.\footnote{Thanks to David Matthews for providing this
@@ -214,7 +214,7 @@
 ML{*PolyML.addPrettyPrinter typ_raw_pretty_printer*}
 
 text {*
-  Now the type bool is printed out as expected.
+  Now the type bool is printed out in full detail.
 
   @{ML_response [display,gray]
   "@{typ \"bool\"}"
@@ -228,7 +228,7 @@
 
   we can see the full name of the type is actually @{text "List.list"}, indicating
   that it is defined in the theory @{text "List"}. However, one has to be 
-  careful with finding out the right name of a type, because even if
+  careful with names of types, because even if
   @{text "fun"}, @{text "bool"} and @{text "nat"} are defined in the 
   theories @{text "HOL"} and @{text "Nat"}, respectively, they are 
   still represented by their simple name.
@@ -674,6 +674,27 @@
   \end{exercise}
 *}
 
+section {* Matching and Unification (TBD) *}
+
+text {* 
+  Using the antiquotation from Section~\ref{sec:antiquote}.
+*}
+
+ML{*val (env, _) = 
+  Sign.typ_unify @{theory} (@{typ_pat "?'b * ?'c"}, @{typ_pat "?'a * ?'b"}) (Vartab.empty, 0) *}
+
+ML{*Vartab.dest env  *}
+
+ML{*Envir.norm_type env @{typ_pat "?'a"}*}
+
+ML{*val env = 
+  Sign.typ_match @{theory} (@{typ_pat "?'b * ?'c"}, @{typ_pat "?'a * ?'b"}) Vartab.empty *}
+
+ML{*Envir.subst_type env  @{typ_pat "?'a"} *}
+
+text {*
+  Note the difference. Norm for unify; Subst for match.
+*}
 
 section {* Type-Checking\label{sec:typechecking} *}