# HG changeset patch
# User paulson
# Date 869563017 -7200
# Node ID acd60238f191eb7e5a1c87772f47beefbfd79e06
# Parent  d4443afc8d289bb1f893fa9b7428461c15349e90
Fixed the spelling of AUTH_NAMES--it could not have worked before\!

diff -r d4443afc8d28 -r acd60238f191 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jul 22 11:15:14 1997 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 22 11:16:57 1997 +0200
@@ -87,7 +87,8 @@
 
 ## Authentication & Security Protocols
 
-Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
+AUTH_NAMES = Message Event Shared NS_Shared \
+	     OtwayRees OtwayRees_AN OtwayRees_Bad \
 	     Recur WooLam Yahalom Yahalom2 \
 	     Public NS_Public_Bad NS_Public TLS