diff -r 2d638e963357 -r 848be46708dc src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -197,6 +197,7 @@
 apply (erule yahalom.induct,
        drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
 apply (simp only: Says_Server_not_range analz_image_freshK_simps)
+apply safe
 done
 
 lemma analz_insert_freshK: