diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Auth/OtwayRees_Bad.thy
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -197,7 +197,7 @@
 
 lemma analz_insert_freshK:
   "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
-      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
+      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
       (K = KAB | Key K \<in> analz (knows Spy evs))"
 by (simp only: analz_image_freshK analz_image_freshK_simps)