# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259770117 -3600
# Node ID f1743ce9dbf14bc61c1fd6074443c43304f1425a
# Parent  ef048892d0f0d696af406c1cb19629a0a343bee9
tuned

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}