src/HOL/Auth/Message.ML

--- a/src/HOL/Auth/Message.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/Message.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -13,8 +13,6 @@
 by (Blast_tac 1);
 Addsimps [result()];
 
-open Message;
-
 AddIffs atomic.inject;
 AddIffs msg.inject;