--- a/Quot/Examples/Larry.thy	Fri Dec 11 06:58:31 2009 +0100
+++ b/Quot/Examples/Larry.thy	Fri Dec 11 08:28:41 2009 +0100
@@ -354,7 +354,7 @@
       and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
       and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
   shows "P msg"
-using N M C D by (blast intro:  msg_induct_aux)
+using N M C D by (rule msg_induct_aux)
 
 subsection{*The Abstract Discriminator*}