src/HOL/Auth/TLS.ML

--- a/src/HOL/Auth/TLS.ML	Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/TLS.ML	Wed Dec 24 10:02:30 1997 +0100
@@ -130,7 +130,7 @@
 (*Nobody sends themselves messages*)
 goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
 by (etac tls.induct 1);
-by (Auto_tac());
+by Auto_tac;
 qed_spec_mp "not_Says_to_self";
 Addsimps [not_Says_to_self];
 AddSEs   [not_Says_to_self RSN (2, rev_notE)];