diff -r d9e0ea61be78 -r 0dc727055c11 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Mon Nov 09 09:48:38 2009 +0100
+++ b/ProgTutorial/General.thy	Mon Nov 09 10:07:08 2009 +0100
@@ -708,7 +708,8 @@
 text {* 
   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?} 
+  instantiations.\footnote{\bf FIXME: what is 0?}  In case of a failure 
+  @{ML typ_unify in Sign} will throw the exception @{ML_text TUNIFY}.
   We can print out the resulting type environment @{ML tyenv_unif} 
   with the built-in function @{ML_ind dest in Vartab}.
 
@@ -771,7 +772,8 @@
 end*}
 
 text {*
-  Printing out the calculated matcher gives
+  In case of failure, @{ML typ_match in Sign} will throw the exception 
+  @{ML_text TYPE_MATCH}. Printing out the calculated matcher gives
 
   @{ML_response_fake [display,gray]
   "pretty_tyenv @{context} tyenv_match"