diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/NS_Public.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -7,8 +7,6 @@
 Version incorporating Lowe's fix (inclusion of B's identify in round 2).
 *)
 
-open NS_Public;
-
 set proof_timing;
 HOL_quantifiers := false;