--- a/ProgTutorial/Essential.thy	Tue May 17 19:46:53 2011 +0200
+++ b/ProgTutorial/Essential.thy	Tue Jun 14 22:09:40 2011 +0100
@@ -1124,13 +1124,14 @@
   as an introduction rule. Applying it directly can lead to unexpected
   behaviour since the unification has more than one solution. One way round
   this problem is to instantiate the schematic variables @{text "?P"} and
-  @{text "?x"}.  instantiation function for theorems is @{ML_ind instantiate
-  in Drule} from the structure @{ML_struct Drule}. One problem, however, is
+  @{text "?x"}.  instantiation function for theorems is 
+  @{ML_ind instantiate_normalize 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 instantiate_normalize in Drule}@{text ":"}
   @{ML_type "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"}
   \end{isabelle}
 
@@ -1183,7 +1184,7 @@
   val trm = @{term \"Trueprop (Q True)\"}
   val inst = matcher_inst @{theory} pat trm 1
 in
-  Drule.instantiate inst @{thm spec}
+  Drule.instantiate_normalize inst @{thm spec}
 end"
   "\<forall>x. Q x \<Longrightarrow> Q True"}