- Instantiated parts_insert_substD to avoid problems with HO unification
- Replaced auto by fastsimp in proof of parts_invKey, since auto looped
because of the new encoding of sets

--- 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