--- a/ProgTutorial/Essential.thy	Tue Nov 24 16:34:39 2009 +0100
+++ b/ProgTutorial/Essential.thy	Tue Nov 24 22:55:44 2009 +0100
@@ -691,7 +691,7 @@
   Section~\ref{sec:antiquote} in order to construct examples involving
   schematic variables.
 
-  Let us begin with describing the unification and matching function for
+  Let us begin with describing the unification and matching functions for
   types.  Both return type environments (ML-type @{ML_type "Type.tyenv"})
   which map schematic type variables to types and sorts. Below we use the
   function @{ML_ind typ_unify in Sign} from the structure @{ML_struct Sign}
@@ -1091,13 +1091,84 @@
   reasonable solution for a unification problem, Isabelle also tries first to
   solve the problem by higher-order pattern unification. 
 
-  For higher-order
-  matching the function is called @{ML_ind matchers in Unify} implemented
-  in the structure @{ML_struct Unify}. Also this
-  function returns sequences with possibly more than one matcher.
-  Like @{ML unifiers in Unify}, this function does not raise an exception
-  in case of failure, but returns an empty sequence. It also first tries 
-  out whether the matching problem can be solved by first-order matching.
+  For higher-order matching the function is called @{ML_ind matchers in Unify}
+  implemented in the structure @{ML_struct Unify}. Also this function returns
+  sequences with possibly more than one matcher.  Like @{ML unifiers in
+  Unify}, this function does not raise an exception in case of failure, but
+  returns an empty sequence. It also first tries out whether the matching
+  problem can be solved by first-order matching.
+
+  Higher-order matching might be necessary for instantiating a theorem
+  appropriately (theorems and their instantiation will be described in more
+  detail in Sections~\ref{sec:theorems}). This is for example the 
+  case when applying the rule @{thm [source] spec}:
+
+  \begin{isabelle}
+  \isacommand{thm}~@{thm [source] spec}\\
+  @{text "> "}~@{thm spec}
+  \end{isabelle}
+
+  as an introduction rule. One way is to instantiate this rule. The
+  instantiation function for theorems is @{ML_ind instantiate in Drule} from
+  the structure @{ML_struct Drule}. One problem, however, is that this 
+  function expects the instantiations as lists of @{ML_type ctyp} and 
+  @{ML_type cterm} pairs:
+
+  \begin{isabelle}
+  @{ML instantiate in Drule}@{text ":"}
+  @{ML_type "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"}
+  \end{isabelle}
+
+  This means we have to transform the environment the higher-order matching 
+  function returns into such an instantiation. For this we use the functions
+  @{ML_ind term_env in Envir} and @{ML_ind type_env in Envir}, which extract
+  from an environment the corresponding variable mappings for schematic type 
+  and term variables. These mappings can be turned into proper 
+  @{ML_type ctyp}-pairs with the function
+*}
+
+ML{*fun prep_trm thy (x, (T, t)) = 
+  (cterm_of thy (Var (x, T)), cterm_of thy t)*} 
+
+text {*
+  and into proper @{ML_type cterm}-pairs with
+*}
+
+ML{*fun prep_ty thy (x, (S, ty)) = 
+  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)*}
+
+text {*
+  We can now calculate the instantiations from the matching function. 
+*}
+
+ML %linenosgray{*fun matcher_inst thy pat trm i = 
+let
+  val univ = Unify.matchers thy [(pat, trm)] 
+  val env = nth (Seq.list_of univ) i
+  val tenv = Vartab.dest (Envir.term_env env)
+  val tyenv = Vartab.dest (Envir.type_env env)
+in
+  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+end*}
+
+text {*
+  In Line 3 we obtain the higher-order matcher. We assume there is a finite
+  number of them and select the one we are interested in via the parameter 
+  @{text i} in the next line. In Lines 5 and 6 we destruct the resulting 
+  environments using the function @{ML_ind dest in Vartab}. Finally, we need 
+  to map the functions @{ML prep_trm} and @{ML prep_ty} over the respective 
+  environments (Line 8). As a simple example we instantiate the 
+  @{thm [source] conjI}-rule as follows
+
+  @{ML_response_fake [gray,display] 
+  "let  
+  val pat = Logic.strip_imp_concl (prop_of @{thm spec})
+  val trm = @{term \"Trueprop (P True)\"}
+  val inst = matcher_inst @{theory} pat trm 1
+in
+  Drule.instantiate inst @{thm conjI}
+end"
+  "\<forall>x. P x \<Longrightarrow> P True"}
 
   \begin{readmore}
   Unification and matching of higher-order patterns is implemented in 
@@ -1289,7 +1360,7 @@
   \end{readmore}
 *}
 
-section {* Theorems *}
+section {* Theorems\label{sec:theorems} *}
 
 text {*
   Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}