--- a/src/HOL/Auth/Guard/P2.thy Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/Auth/Guard/P2.thy Fri Oct 07 20:41:10 2005 +0200
@@ -302,7 +302,7 @@
==> (Key (priK A):parts (knows (Friend B) evs)) --> (A:bad)"
apply (erule p2.induct)
apply (simp_all add: initState.simps knows.simps pro_def prom_def
- req_def reqm_def anchor_def chain_def sign_def, blast)
+ req_def reqm_def anchor_def chain_def sign_def)
apply (blast dest: no_Key_in_agl)
apply (auto del: parts_invKey disjE dest: parts_trans
simp add: no_Key_in_appdel)