# HG changeset patch
# User wenzelm
# Date 978553148 -3600
# Node ID a7282df327c6e596b9be34612a63b6d2b2af13f6
# Parent  8fa4aafa73143937380509af10744fbc5af124b9
tuned;

diff -r 8fa4aafa7314 -r a7282df327c6 src/HOL/Subst/Unify.ML
--- 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.
  *---------------------------------------------------------------------------*)