diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/OtwayRees_Bad.thy
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Tue Sep 23 15:41:33 2003 +0200
@@ -90,15 +90,16 @@
 declare Fake_parts_insert_in_Un  [dest]
 
 (*A "possibility property": there are traces that reach the end*)
-lemma "B \<noteq> Server
-      ==> \<exists>K. \<exists>NA. \<exists>evs \<in> otway.
+lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
+      ==> \<exists>NA. \<exists>evs \<in> otway.
             Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
               \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] otway.Nil
                     [THEN otway.OR1, THEN otway.Reception,
                      THEN otway.OR2, THEN otway.Reception,
-                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
+                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
+apply (possibility, simp add: used_Cons) 
 done
 
 lemma Gets_imp_Says [dest!]: