--- a/src/HOL/Subst/Unify.ML Wed Jan 03 21:18:31 2001 +0100
+++ b/src/HOL/Subst/Unify.ML Wed Jan 03 21:19:08 2001 +0100
@@ -31,10 +31,6 @@
* Deeper nestings require iteration of steps (3) and (4).
*---------------------------------------------------------------------------*)
-open Unify;
-
-
-
(*---------------------------------------------------------------------------
* The non-nested TC plus the wellfoundedness of unifyRel.
*---------------------------------------------------------------------------*)