diff -r 7f7080ce7c2b -r d7d55a5030b5 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Fri Nov 20 03:03:04 2009 +0100
+++ b/ProgTutorial/Essential.thy	Sat Nov 21 00:29:43 2009 +0100
@@ -819,7 +819,7 @@
   "[?'a := ?'b list, ?'b := nat]"}
 
   Observe that the type environment which the function @{ML typ_unify in
-  Sign} returns is in \emph{not} an instantiation in fully solved form: while @{text
+  Sign} returns is \emph{not} an instantiation in fully solved form: while @{text
   "?'b"} is instantiated to @{typ nat}, this is not propagated to the
   instantiation for @{text "?'a"}.  In unification theory, this is often
   called an instantiation in \emph{triangular form}. These triangular 
@@ -859,7 +859,7 @@
   "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"
   "bool list * nat"}
 
-  Be careful to observe the difference: use always 
+  Be careful to observe the difference: always use
   @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir} 
   for unifiers. To show the difference, let us calculate the 
   following matcher:
@@ -935,7 +935,7 @@
 end *}
 
 text {*
-  In this example we annotated explicitly types because then 
+  In this example we annotated types explicitly because then 
   the type environment is empty and can be ignored. The 
   resulting term environment is
 
@@ -960,7 +960,7 @@
   "P (\<lambda>a b. Q b a)"}
 
   First-order matching is useful for matching against applications and
-  variables. It can deal also with abstractions and a limited form of
+  variables. It can also deal with abstractions and a limited form of
   alpha-equivalence, but this kind of matching should be used with care, since
   it is not clear whether the result is meaningful. A meaningful example is
   matching @{text "\<lambda>x. P x"} against the pattern @{text "\<lambda>y. ?X y"}. In this
@@ -984,8 +984,8 @@
   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 or a free
-  variable. If it is a schematic variable then it can be only applied with
-  distinct bound variables. This excludes terms where a schematic variable is an
+  variable. If it is a schematic variable then it can only have distinct bound 
+  variables as arguments. 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