diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 12901333de..879478ce02 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -165,12 +165,12 @@ inductiveSyntaxToView modifiers decl 2
 
 def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
 v ← inductiveSyntaxToView modifiers stx;
-elabInductiveCore #[v]
+elabInductiveViews #[v]
 
 def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
 let modifiers := modifiers.addAttribute { name := `class };
 v ← classInductiveSyntaxToView modifiers stx;
-elabInductiveCore #[v]
+elabInductiveViews #[v]
 
 @[builtinCommandElab declaration]
 def elabDeclaration : CommandElab :=
@@ -213,7 +213,7 @@ views ← elems.mapM $ fun stx => do {
    modifiers ← elabModifiers (stx.getArg 0);
    inductiveSyntaxToView modifiers (stx.getArg 1)
 };
-elabInductiveCore views
+elabInductiveViews views
 
 private def isMutualPreambleCommand (stx : Syntax) : Bool :=
 let k := stx.getKind;
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index ec6d235769..b0eec274f2 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -485,7 +485,7 @@ views.forM fun view => do {
   pure ()
 }
 
-def elabInductiveCore (views : Array InductiveView) : CommandElabM Unit := do
+def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
 let view0 := views.get! 0;
 let ref   := view0.ref;
 decl ← runTermElabM view0.declName $ fun vars => mkInductiveDecl vars views;
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 021d55b053..21a6e5568f 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -71,7 +71,7 @@ else do
   declName ← applyVisibility ctor modifiers.visibility declName;
   pure { ref := ctor, name := name, modifiers := modifiers, inferMod := inferMod, declName := declName }
 
-private def elabStructView (view : StructView) : TermElabM ElabStructResult :=
+private def elabStructureView (view : StructView) : TermElabM ElabStructResult :=
 throw $ arbitrary _ -- TODO
 
 /-
@@ -102,7 +102,7 @@ withDeclId declId $ fun name => do
   declName ← mkDeclName declId modifiers name;
   ctor ← expandCtor stx declName;
   allUserLevelNames ← getLevelNames;
-  r ← runTermElabM declName $ fun scopeVars => Term.elabBinders params $ fun params => elabStructView {
+  r ← runTermElabM declName $ fun scopeVars => Term.elabBinders params $ fun params => elabStructureView {
     ref               := stx,
     modifiers         := modifiers,
     scopeLevelNames   := scopeLevelNames,