diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 0e50b1b933..c6d15e7baa 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.Util.CollectLevelParams
 import Lean.Elab.DeclUtil
-import Lean.Elab.Definition
+import Lean.Elab.DefView
 import Lean.Elab.Inductive
 import Lean.Elab.Structure
 import Lean.Elab.MutualDef
diff --git a/src/Lean/Elab/Definition.lean b/src/Lean/Elab/DefView.lean
similarity index 100%
rename from src/Lean/Elab/Definition.lean
rename to src/Lean/Elab/DefView.lean
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index c4fe858110..6d56e899d9 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -9,7 +9,7 @@ import Lean.Util.CollectLevelParams
 import Lean.Util.Constructions
 import Lean.Elab.Command
 import Lean.Elab.CollectFVars
-import Lean.Elab.Definition
+import Lean.Elab.DefView
 import Lean.Elab.DeclUtil
 
 namespace Lean
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 261db49e29..aa51e31688 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Meta.Closure
 import Lean.Meta.Check
 import Lean.Elab.Command
-import Lean.Elab.Definition
+import Lean.Elab.DefView
 
 namespace Lean
 namespace Elab