
diff -r 78c91a629602 -r 5f7ca76f94e3 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Wed Nov 11 12:15:48 2009 +0100
+++ b/ProgTutorial/General.thy	Thu Nov 12 10:06:26 2009 +0100
@@ -677,7 +677,7 @@
 section {* Unification and Matching *}
 
 text {* 
-  Isabelle's terms and types may contain schematic term variables
+  As seen earlier, Isabelle's terms and types may contain schematic term variables
   (term-constructor @{ML Var}) and schematic type variables (term-constructor
   @{ML TVar}). These variables stand for unknown entities, which can be made
   more concrete by instantiations. Such instantiations might be a result of
@@ -708,10 +708,10 @@
 text {* 
   The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type
   environment, which is needed for starting the unification without any
-  (pre)instantiations. The @{text 0} is an integer index that we will explain
+  (pre)instantiations. The @{text 0} is an integer index that will be explained
   below. In case of failure @{ML typ_unify in Sign} will throw the exception
-  @{text TUNIFY}.  We can print out the resulting type environment @{ML
-  tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
+  @{text TUNIFY}.  We can print out the resulting type environment bound to 
+  @{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
   structure @{ML_struct Vartab}.
 
   @{ML_response_fake [display,gray]
@@ -750,10 +750,11 @@
 text {*
   The first components in this list stand for the schematic type variables and
   the second are the associated sorts and types. In this example the sort is
-  the default sort @{text "HOL.type"}. We will use in what follows the
-  pretty-printing function from Figure~\ref{fig:prettyenv} for @{ML_type
-  "Type.tyenv"}s. For the type environment in the example this function prints
-  out the more legible:
+  the default sort @{text "HOL.type"}. Instead of @{ML "Vartab.dest"}, we will
+  use in what follows our own pretty-printing function from
+  Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s. For the type
+  environment in the example this function prints out the more legible:
+
 
   @{ML_response_fake [display, gray]
   "pretty_tyenv @{context} tyenv_unif"
@@ -808,8 +809,8 @@
   "index"
   "1"}
 
-  Let us now return again to the unification problem @{text "?'a * ?'b"} and 
-  @{text "?'b list * nat"} from the beginning of the section, and the 
+  Let us now return to the unification problem @{text "?'a * ?'b"} and 
+  @{text "?'b list * nat"} from the beginning of this section, and the 
   calculated type environment @{ML tyenv_unif}:
 
   @{ML_response_fake [display, gray]
@@ -820,18 +821,15 @@
   Sign} returns is in \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 not fully solved 
-  instantiations are used because of performance reasons.
-  To apply a type environment in triangular form to a type, say @{text "?'a *
+  called an instantiation in \emph{triangular form}. These triangular 
+  instantiations, or triangular type environments, are used because of 
+  performance reasons. To apply such a type environment to a type, say @{text "?'a *
   ?'b"}, you should use the function @{ML_ind norm_type in Envir}:
 
   @{ML_response_fake [display, gray]
   "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
   "nat list * nat"}
 
-  With this function the type variables @{text "?'a"} and @{text "?'b"} are 
-  correctly instantiated.
-
   Matching of types can be done with the function @{ML_ind typ_match in Sign}
   also from the structure @{ML_struct Sign}. This function returns a @{ML_type
   Type.tyenv} as well, but might raise the exception @{text TYPE_MATCH} in case
@@ -854,7 +852,7 @@
   
   Unlike unification, which uses the function @{ML norm_type in Envir}, 
   applying the matcher to a type needs to be done with the function
-  @{ML_ind subst_type in Envir}.
+  @{ML_ind subst_type in Envir}. For example
 
   @{ML_response_fake [display, gray]
   "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"
@@ -862,7 +860,7 @@
 
   Be careful to observe the difference: use always 
   @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir} 
-  for unifiers. To make the difference explicit, let us calculate the 
+  for unifiers. To show the difference, let us calculate the 
   following matcher:
 *}
 
@@ -896,7 +894,7 @@
   are in @{ML_file "Pure/sign.ML"}. Matching and unification produce type environments
   as results. These are implemented in @{ML_file "Pure/envir.ML"}.
   This file also includes the substitution and normalisation functions,
-  that apply a type environment to a type. Type environments are lookup 
+  which apply a type environment to a type. Type environments are lookup 
   tables which are implemented in @{ML_file "Pure/term_ord.ML"}.
   \end{readmore}
 *}
@@ -984,8 +982,8 @@
   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 a lambda term whose ``head symbol'' (that is the
-  first symbol under abstractions) is either a constant, or a schematic or a free
-  variable. If it is a schematic variable then it can be only applied by
+  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 that a schematic variable is an
   argument of another one and that a schematic variable is applied
   twice with the same bound variable. The function @{ML_ind pattern in Pattern}
@@ -1009,8 +1007,8 @@
   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 maxind, a type environment 
-  and a term environment). The former function is @{ML_ind match in Pattern},
-  the latter @{ML_ind unify in Pattern} both implemented in the structure
+  and a term environment). The corresponding functions are @{ML_ind match in Pattern},
+  and @{ML_ind unify in Pattern} both implemented in the structure
   @{ML_struct Pattern}. An example for higher-order pattern unification is
 
   @{ML_response_fake [display, gray]
@@ -1029,29 +1027,25 @@
   already the same type. In case of failure, the exceptions that are raised
   are either @{text Pattern}, @{text MATCH} or @{text Unif}.
 
-  As mentioned before, ``full'' higher-order unification, respectively, matching 
-  problems are in general undecidable and might in general not posses a single
-  most general solution. Therefore Isabelle implements Huet's pre-unification
-  algorithm which does not return a single result, rather a lazy list of potentially
-  infinite unifiers. The corresponding function is called @{ML_ind unifiers in Unify}.
-  An example is as follows
+  As mentioned before, ``full'' higher-order unification, respectively
+  higher-order matching problems, are in general undecidable and might also not posses a
+  single most general solution. Therefore Isabelle implements the unification
+  function @{ML_ind unifiers in Unify} so that it returns a lazy list of
+  potentially infinite unifiers.  An example is as follows
 
   \ldots
 
   In case of failure this function does not raise an exception, rather returns
   the empty sequence. In order to find a reasonable solution for a unification 
   problem, Isabelle also tries first to solve the problem by higher-order 
-  pattern unification.
+  pattern unification. For higher-order matching the function is called 
+  @{ML_ind matchers in Unify}. Also this function might potentially return 
+  sequences with more than one matcher.
 
   \ldots
-  
-  For higher-order matching the function is called @{ML_ind matchers in Unify}.
-  Also this function might potentially return sequences with more than one
-  element.
-
 
   Like @{ML unifiers in Unify}, this function does not raise an exception
-  in case of failure. It also tries out first whether the matching problem
+  in case of failure. It also first tries out whether the matching problem
   can be solved by first-order matching.
 
   \begin{readmore}




