src/HOL/Auth/Guard/Analz.thy

 ==> Nonce n:kparts {Y} --> Nonce n:analz G"
 by (erule synth.induct, auto)
 
 lemma kparts_insert_synth: "[| Y:parts (insert X G); X:synth (analz G);
 Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Y:parts G"
-apply (drule parts_insert_substD [where P="%S. Y : S"], clarify)
+apply (drule parts_insert_substD, clarify)
 apply (drule in_sub, drule_tac X=Y in parts_sub, simp)
-by (auto dest: Nonce_kparts_synth)
+apply (auto dest: Nonce_kparts_synth)
+done
 
 lemma Crypt_insert_synth:
   "[| Crypt K Y:parts (insert X G); X:synth (analz G); Nonce n:kparts {Y}; Nonce n ~:analz G |] 
    ==> Crypt K Y:parts G"
 by (metis Fake_parts_insert_in_Un Nonce_kparts_synth UnE analz_conj_parts synth_simps(5))