src/HOL/Auth/NS_Public_Bad.ML

--- a/src/HOL/Auth/NS_Public_Bad.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -29,7 +29,7 @@
 (**** Inductive proofs about ns_public ****)
 
 (*Nobody sends themselves messages*)
-Goal "evs : ns_public ==> ALL A X. Says A A X ~: set evs";
+Goal "evs : ns_public ==> ALL X. Says A A X ~: set evs";
 by (etac ns_public.induct 1);
 by Auto_tac;
 qed_spec_mp "not_Says_to_self";