--- 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;