# HG changeset patch
# User blanchet
# Date 1332247989 -3600
# Node ID 7be54568efa12b5cee053c7a8f5b4dce3fb9395a
# Parent  72bd3311ecba15d52e45c09da5ff02e7c8d31830
optimized "metis" call

diff -r 72bd3311ecba -r 7be54568efa1 src/HOL/Auth/KerberosV.thy
--- a/src/HOL/Auth/KerberosV.thy	Tue Mar 20 13:53:09 2012 +0100
+++ b/src/HOL/Auth/KerberosV.thy	Tue Mar 20 13:53:09 2012 +0100
@@ -680,7 +680,7 @@
 txt{*K4*}
 apply (force dest!: Crypt_imp_keysFor)
 txt{*K6*}
-apply (metis Says_imp_spies Says_ticket_parts analz.Fst analz.Inj analz_conj_parts unique_CryptKey)
+apply (metis MPair_parts Says_imp_parts_knows_Spy unique_CryptKey)
 done
 
 text{*Needs a unicity theorem, hence moved here*}