--- a/src/HOL/Auth/Guard/Extensions.thy Wed May 07 10:59:18 2008 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy Wed May 07 10:59:19 2008 +0200
@@ -206,7 +206,7 @@
lemma parts_invKey [rule_format,dest]:"X:parts {Y} ==>
X:analz (insert (Crypt K Y) H) --> X ~:analz H --> Key (invKey K):analz H"
-by (erule parts.induct, auto dest: parts.Fst parts.Snd parts.Body)
+by (erule parts.induct, (fastsimp dest: parts.Fst parts.Snd parts.Body)+)
lemma in_analz: "Y:analz H ==> EX X. X:H & Y:parts {X}"
by (erule analz.induct, auto intro: parts.Fst parts.Snd parts.Body)
@@ -215,7 +215,7 @@
lemma Crypt_synth_insert: "[| Crypt K X:parts (insert Y H);
Y:synth (analz H); Key K ~:analz H |] ==> Crypt K X:parts H"
-apply (drule parts_insert_substD, clarify)
+apply (drule parts_insert_substD [where P="%S. Crypt K X : S"], clarify)
apply (frule in_sub)
apply (frule parts_mono)
by auto