src/HOL/UNITY/NSP_Bad.ML

--- a/src/HOL/UNITY/NSP_Bad.ML	Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/NSP_Bad.ML	Tue May 04 10:26:00 1999 +0200
@@ -67,8 +67,8 @@
 
 (*Spy never sees another agent's private key! (unless it's bad at start)*)
 (*
-    Goal "Nprg : Invariant {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
-    by (rtac InvariantI 1);
+    Goal "Nprg : Always {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
+    by (rtac AlwaysI 1);
     by (Force_tac 1);
     by (constrains_tac 1);
     by Auto_tac;