diff -r 315694e22856 -r e85c24717cad src/HOL/Auth/NS_Public.thy
--- a/src/HOL/Auth/NS_Public.thy	Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Thu Jun 26 13:20:50 1997 +0200
@@ -32,16 +32,15 @@
          (*Bob responds to Alice's message with a further nonce*)
     NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
              Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
-               : set_of_list evs |]
+               : set evs |]
           ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
                 # evs  :  ns_public"
 
          (*Alice proves her existence by sending NB back to Bob.*)
     NS3  "[| evs: ns_public;  A ~= B;
-             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
-               : set_of_list evs;
+             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
              Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
-               : set_of_list evs |]
+               : set evs |]
           ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
 
   (**Oops message??**)