--- a/ProgTutorial/Tactical.thy	Mon Jan 16 07:40:17 2012 +0000
+++ b/ProgTutorial/Tactical.thy	Wed Feb 15 14:33:29 2012 +0000
@@ -796,7 +796,7 @@
   "\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"}
 
   If you need to instantiate lists of theorems, you can use the
-  functions @{ML_ind RL in Drule} and @{ML_ind MRL in Drule}. For 
+  functions @{ML_ind RL in Drule} and @{ML_ind OF in Drule}. For 
   example in the code below, every theorem in the second list is 
   instantiated with every theorem in the first.