--- a/src/HOL/Auth/Recur.thy Tue Apr 29 12:36:40 2003 +0200
+++ b/src/HOL/Auth/Recur.thy Tue Apr 29 12:36:49 2003 +0200
@@ -392,8 +392,8 @@
apply blast
txt{*Inductive step of respond*}
apply (intro allI conjI impI, simp_all)
-txt{*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*}
-apply (blast dest: unique_session_keys [OF _ respond_certificate])
+txt{*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*}
+apply (blast dest: unique_session_keys respond_certificate)
apply (blast dest!: respond_certificate)
apply (blast dest!: resp_analz_insert)
done