diff -r c2dde8c7174f -r d04d1cd0e058 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Sat May 29 21:30:08 2010 +0200
+++ b/ProgTutorial/Essential.thy	Mon May 31 22:27:48 2010 +0200
@@ -970,14 +970,14 @@
 text {*
   Unification of abstractions is more thoroughly studied in the context of
   higher-order pattern unification and higher-order pattern matching.  A
-  \emph{\index*{pattern}} is an abstraction term whose ``head symbol'' (that
-  is the first symbol under an abstraction) is either a constant, a schematic
-  variable or a free variable. If it is a schematic variable then it can only
-  have distinct bound variables as arguments. This excludes terms where a
+  \emph{\index*{pattern}} is a well-formed beta-normal term in which the arguments to
+  every schematic variable are distinct bounds.
+  In particular this excludes terms where a
   schematic variable is an argument of another one and where a schematic
   variable is applied twice with the same bound variable. The function
   @{ML_ind pattern in Pattern} in the structure @{ML_struct Pattern} tests
-  whether a term satisfies these restrictions.
+  whether a term satisfies these restrictions under the assumptions
+  that it is beta-normal, well-typed and has no loose bound variables.
 
   @{ML_response [display, gray]
   "let
@@ -993,6 +993,9 @@
 
   The point of the restriction to patterns is that unification and matching 
   are decidable and produce most general unifiers, respectively matchers. 
+  Note that \emph{both} terms to be unified have to be higher-order patterns
+  for this to work. The exception @{ML_ind Pattern in Pattern} indicates failure
+  in this regard.
   In this way, matching and unification can be implemented as functions that 
   produce a type and term environment (unification actually returns a 
   record of type @{ML_type Envir.env} containing a max-index, a type environment