--- a/ProgTutorial/Essential.thy	Wed Dec 02 03:46:32 2009 +0100
+++ b/ProgTutorial/Essential.thy	Wed Dec 02 17:06:41 2009 +0100
@@ -1087,9 +1087,20 @@
 end"
 "NONE"}
 
-  In order to find a
-  reasonable solution for a unification problem, Isabelle also tries first to
-  solve the problem by higher-order pattern unification. 
+  In order to find a reasonable solution for a unification problem, Isabelle
+  also tries first to solve the problem by higher-order pattern
+  unification. Only in case of failure full higher-order unification is
+  called. This function has a built-in bound, which can be accessed and
+  manipulated as a configuration value:
+
+  @{ML_response_fake [display,gray]
+  "Config.get_thy @{theory} (Unify.search_bound_value)"
+  "Int 60"}
+
+  If this bound is reached during unification, Isabelle prints out the
+  warning message @{text [quotes] "Unification bound exceeded"} and
+  plenty of diagnostic information. 
+
 
   For higher-order matching the function is called @{ML_ind matchers in Unify}
   implemented in the structure @{ML_struct Unify}. Also this function returns