diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 6ae70ae111..eab58446d1 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -157,6 +157,7 @@ fun stx => match expandDeclNamespace? stx with
   else if declKind == `Lean.Parser.Command.structure then
     elabStructure modifiers decl
   else if isDefLike decl then do
+    -- TODO: use `elabMutualDef #[stx]`
     view ← mkDefView modifiers decl;
     elabDefLike view
   else
diff --git a/src/Lean/Elab/Definition.lean b/src/Lean/Elab/Definition.lean
index 4516c9a717..046aaf4ad0 100644
--- a/src/Lean/Elab/Definition.lean
+++ b/src/Lean/Elab/Definition.lean
@@ -14,9 +14,6 @@ import Lean.Elab.DeclUtil
 
 namespace Lean
 namespace Elab
-namespace Command
-
-open Meta
 
 inductive DefKind
 | «def» | «theorem» | «example» | «opaque» | «abbrev»
@@ -44,6 +41,10 @@ structure DefView :=
 (type?         : Option Syntax)
 (val           : Syntax)
 
+namespace Command
+
+open Meta
+
 def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView :=
 -- parser! "abbrev " >> declId >> optDeclSig >> declVal
 let (binders, type) := expandOptDeclSig (stx.getArg 2);
@@ -133,6 +134,8 @@ else if declKind == `Lean.Parser.Command.«example» then
 else
   throwError "unexpected kind of definition"
 
+/- TODO Remove the rest of the file after we finish `MutualDef.lean`, and rename it to `DefView.lean` -/
+
 private def removeUnused (vars : Array Expr) (xs : Array Expr) (e : Expr) (eType : Expr)
     : TermElabM (LocalContext × LocalInstances × Array Expr) := do
 let used : CollectFVars.State := {};
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 664675a608..99c4a0cf5d 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -9,10 +9,11 @@ import Lean.Elab.Definition
 namespace Lean
 namespace Elab
 
-structure MutualDefView :=
+/- DefView after elaborating the header. -/
+structure DefViewElabHeader :=
 (ref           : Syntax)
 (modifiers     : Modifiers)
-(kind          : Command.DefKind)
+(kind          : DefKind)
 (shortDeclName : Name)
 (declName      : Name)
 (levelNames    : List Name)
@@ -23,7 +24,6 @@ structure MutualDefView :=
 namespace Term
 
 open Meta
-open Command (DefView)
 
 def checkModifiers (m₁ m₂ : Modifiers) : TermElabM Unit := do
 unless (m₁.isUnsafe == m₂.isUnsafe) $
@@ -34,9 +34,9 @@ unless (m₁.isPartial == m₂.isPartial) $
   throwError "cannot mix partial and non-partial definitions";
 pure ()
 
-def elabHeaders (views : Array DefView) : TermElabM (Array MutualDefView) :=
+def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHeader) :=
 views.foldlM
-  (fun (headers : Array MutualDefView) (view : DefView) => withRef view.ref do
+  (fun (headers : Array DefViewElabHeader) (view : DefView) => withRef view.ref do
     currNamespace ← getCurrNamespace;
     currLevelNames ← getLevelNames;
     ⟨shortDeclName, declName, levelNames⟩ ← expandDeclId currNamespace currLevelNames view.declId view.modifiers;