diff --git a/src/Init/Lean/Elab.lean b/src/Init/Lean/Elab.lean
index 2bd5bc3852..08848508d1 100644
--- a/src/Init/Lean/Elab.lean
+++ b/src/Init/Lean/Elab.lean
@@ -6,11 +6,11 @@ Authors: Leonardo de Moura
 prelude
 import Init.Lean.Elab.Import
 import Init.Lean.Elab.Exception
-import Init.Lean.Elab.ElabStrategyAttrs
+import Init.Lean.Elab.StrategyAttrs
 import Init.Lean.Elab.Command
 import Init.Lean.Elab.Term
-import Init.Lean.Elab.TermApp
-import Init.Lean.Elab.TermBinders
+import Init.Lean.Elab.App
+import Init.Lean.Elab.Binders
 import Init.Lean.Elab.Quotation
 import Init.Lean.Elab.Frontend
 import Init.Lean.Elab.BuiltinNotation
diff --git a/src/Init/Lean/Elab/TermApp.lean b/src/Init/Lean/Elab/App.lean
similarity index 100%
rename from src/Init/Lean/Elab/TermApp.lean
rename to src/Init/Lean/Elab/App.lean
diff --git a/src/Init/Lean/Elab/TermBinders.lean b/src/Init/Lean/Elab/Binders.lean
similarity index 100%
rename from src/Init/Lean/Elab/TermBinders.lean
rename to src/Init/Lean/Elab/Binders.lean
diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index c191687ba6..17c127d84c 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -8,8 +8,8 @@ import Init.Lean.Elab.Alias
 import Init.Lean.Elab.Log
 import Init.Lean.Elab.ResolveName
 import Init.Lean.Elab.Term
-import Init.Lean.Elab.TermBinders
-import Init.Lean.Elab.SynthesizeSyntheticMVars
+import Init.Lean.Elab.Binders
+import Init.Lean.Elab.SyntheticMVars
 
 namespace Lean
 namespace Elab
diff --git a/src/Init/Lean/Elab/Definition.lean b/src/Init/Lean/Elab/Definition.lean
index b1fc21ac07..85298bd714 100644
--- a/src/Init/Lean/Elab/Definition.lean
+++ b/src/Init/Lean/Elab/Definition.lean
@@ -7,7 +7,7 @@ prelude
 import Init.Lean.Util.CollectLevelParams
 import Init.Lean.Util.CollectFVars
 import Init.Lean.Elab.DeclModifiers
-import Init.Lean.Elab.TermBinders
+import Init.Lean.Elab.Binders
 
 namespace Lean
 namespace Elab
diff --git a/src/Init/Lean/Elab/DoNotation.lean b/src/Init/Lean/Elab/DoNotation.lean
index 0ce165703f..e476772226 100644
--- a/src/Init/Lean/Elab/DoNotation.lean
+++ b/src/Init/Lean/Elab/DoNotation.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Lean.Elab.Term
-import Init.Lean.Elab.TermBinders
+import Init.Lean.Elab.Binders
 import Init.Lean.Elab.Quotation
 
 namespace Lean
diff --git a/src/Init/Lean/Elab/ElabStrategyAttrs.lean b/src/Init/Lean/Elab/StrategyAttrs.lean
similarity index 100%
rename from src/Init/Lean/Elab/ElabStrategyAttrs.lean
rename to src/Init/Lean/Elab/StrategyAttrs.lean
diff --git a/src/Init/Lean/Elab/StructInst.lean b/src/Init/Lean/Elab/StructInst.lean
index 9bcd71e631..495eb8c6ec 100644
--- a/src/Init/Lean/Elab/StructInst.lean
+++ b/src/Init/Lean/Elab/StructInst.lean
@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Elab.Term
-import Init.Lean.Elab.TermApp
-import Init.Lean.Elab.TermBinders
+import Init.Lean.Elab.App
+import Init.Lean.Elab.Binders
 import Init.Lean.Elab.Quotation
 
 namespace Lean
diff --git a/src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean b/src/Init/Lean/Elab/SyntheticMVars.lean
similarity index 100%
rename from src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean
rename to src/Init/Lean/Elab/SyntheticMVars.lean
diff --git a/src/Init/Lean/Elab/Tactic/ElabTerm.lean b/src/Init/Lean/Elab/Tactic/ElabTerm.lean
index 60bed64a4b..9f9856db08 100644
--- a/src/Init/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Init/Lean/Elab/Tactic/ElabTerm.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Lean.Meta.Tactic.Apply
 import Init.Lean.Elab.Tactic.Basic
-import Init.Lean.Elab.SynthesizeSyntheticMVars
+import Init.Lean.Elab.SyntheticMVars
 
 namespace Lean
 namespace Elab