# HG changeset patch
# User berghofe
# Date 1210150758 -7200
# Node ID d334a6d695982c16996e5bb2bc7c33cd8c93bc01
# Parent  4cd176ea28dcc488733aed807ae477a69cf64186
Instantiated parts_insert_substD to avoid problems with HO unification

diff -r 4cd176ea28dc -r d334a6d69598 src/HOL/Auth/Guard/Analz.thy
--- a/src/HOL/Auth/Guard/Analz.thy	Wed May 07 10:59:02 2008 +0200
+++ b/src/HOL/Auth/Guard/Analz.thy	Wed May 07 10:59:18 2008 +0200
@@ -243,13 +243,13 @@
 
 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, clarify)
+apply (drule parts_insert_substD [where P="%S. Y : S"], clarify)
 apply (drule in_sub, drule_tac X=Y in parts_sub, simp)
 by (auto dest: Nonce_kparts_synth)
 
 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"
-apply (drule parts_insert_substD, clarify)
+apply (drule parts_insert_substD [where P="%S. Crypt K Y : S"], clarify)
 apply (drule in_sub, drule_tac X="Crypt K Y" in parts_sub, simp, clarsimp)
 apply (ind_cases "Crypt K Y:synth (analz G)")
 by (auto dest: Nonce_kparts_synth)