diff --git a/library/logic/wf.lean b/library/logic/wf.lean
index 6af3b2db12..4063bdb429 100644
--- a/library/logic/wf.lean
+++ b/library/logic/wf.lean
@@ -1,7 +1,7 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic
+import logic.eq
 
 inductive acc {A : Type} (R : A → A → Prop) : A → Prop :=
 intro : ∀x, (∀ y, R y x → acc R y) → acc R x