--- a/ProgTutorial/Tactical.thy	Tue May 17 19:46:53 2011 +0200
+++ b/ProgTutorial/Tactical.thy	Tue Jun 14 22:09:40 2011 +0100
@@ -876,7 +876,7 @@
   @{thm [source] rule}. For this the function @{ML_ind first_order_match in Thm} 
   matches two @{ML_type cterm}s and produces, in the successful case, a matcher 
   that can be used to instantiate the theorem. The instantiation 
-  can be done with the function @{ML_ind instantiate in Drule}. To automate 
+  can be done with the function @{ML_ind instantiate_normalize in Drule}. To automate 
   this we implement the following function.
 *}
 
@@ -885,7 +885,7 @@
     val concl_pat = Drule.strip_imp_concl (cprop_of thm)
     val insts = Thm.first_order_match (concl_pat, concl)
   in
-    rtac (Drule.instantiate insts thm) 1
+    rtac (Drule.instantiate_normalize insts thm) 1
   end)*}
 
 text {*