diff -r ef048892d0f0 -r f1743ce9dbf1 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Wed Dec 02 17:06:41 2009 +0100
+++ b/ProgTutorial/Essential.thy	Wed Dec 02 17:08:37 2009 +0100
@@ -1099,7 +1099,8 @@
 
   If this bound is reached during unification, Isabelle prints out the
   warning message @{text [quotes] "Unification bound exceeded"} and
-  plenty of diagnostic information. 
+  plenty of diagnostic information (sometimes annoyingly plenty of 
+  information). 
 
 
   For higher-order matching the function is called @{ML_ind matchers in Unify}