diff -r 75ea0e390a92 -r d1d79f0e1ea6 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Auth/Message.thy	Fri Aug 12 14:45:50 2011 -0700
@@ -841,7 +841,7 @@
 apply (erule analz.induct, auto)
 apply (blast dest:parts.Body)
 apply (blast dest: parts.Body)
-apply (metis Un_absorb2 keyfree_KeyE mem_def parts_Un parts_keyfree sup1I2)
+apply (metis Un_absorb2 keyfree_KeyE parts_Un parts_keyfree UnI2)
 done
 
 subsection{*Tactics useful for many protocol proofs*}