diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/Recur.thy	Fri Jun 27 10:47:13 1997 +0200
@@ -90,15 +90,13 @@
            those in the message he previously sent the Server.*)
     RA4  "[| evs: recur lost;  A ~= B;  
              Says B  C {|XH, Agent B, Agent C, Nonce NB, 
-                         XA, Agent A, Agent B, Nonce NA, P|} 
-               : set evs;
+                         XA, Agent A, Agent B, Nonce NA, P|} : set evs;
              Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
                          Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
-                         RA|}
-               : set evs |]
+                         RA|} : set evs |]
           ==> Says B A RA # evs : recur lost"
 
-(**No "oops" message can readily be expressed, since each session key is
+(**No "oops" message can easily be expressed.  Each session key is
    associated--in two separate messages--with two nonces.
 ***)
 end