diff --git a/src/Init/Lean/Elaborator/Basic.lean b/src/Init/Lean/Elaborator/Basic.lean
index 375aa4276c..03c8110a0c 100644
--- a/src/Init/Lean/Elaborator/Basic.lean
+++ b/src/Init/Lean/Elaborator/Basic.lean
@@ -123,7 +123,7 @@ match attrParamSyntaxToIdentifier arg with
 def declareBuiltinElab (env : Environment) (addFn : Name) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
 let name := `_regBuiltinTermElab ++ declName;
 let type := mkApp (mkConst `IO) (mkConst `Unit);
-let val  := mkCAppN addFn #[toExpr kind, toExpr declName, mkConst declName];
+let val  := mkAppN (mkConst addFn) #[toExpr kind, toExpr declName, mkConst declName];
 let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
 match env.addAndCompile {} decl with
 -- TODO: pretty print error
diff --git a/src/Init/Lean/Expr.lean b/src/Init/Lean/Expr.lean
index 4ac26b3ed6..baf00c463c 100644
--- a/src/Init/Lean/Expr.lean
+++ b/src/Init/Lean/Expr.lean
@@ -330,9 +330,6 @@ Expr.localE x u t $ mkDataForBinder (mixHash 43 $ hash t) t.looseBVarRange true
 @[export lean_expr_mk_proj] def mkProjEx : Name → Nat → Expr → Expr := mkProj
 @[export lean_expr_mk_local] def mkLocalEx : Name → Name → Expr → BinderInfo → Expr := mkLocal
 
-def mkCApp (f : Name) (a : Expr) : Expr :=
-mkApp (mkConst f) a
-
 def mkAppN (f : Expr) (args : Array Expr) : Expr :=
 args.foldl mkApp f
 
@@ -583,9 +580,6 @@ instance : HasRepr Expr :=
 
 end Expr
 
-def mkCAppN (n : Name) (args : Array Expr) : Expr :=
-mkAppN (mkConst n) args
-
 def mkAppB (f a b : Expr) := mkApp (mkApp f a) b
 def mkApp2 (f a b : Expr) := mkAppB f a b
 def mkApp3 (f a b c : Expr) := mkApp (mkAppB f a b) c
@@ -597,7 +591,6 @@ def mkApp8 (f a b c d e₁ e₂ e₃ e₄ : Expr) := mkApp4 (mkApp4 f a b c d) e
 def mkApp9 (f a b c d e₁ e₂ e₃ e₄ e₅ : Expr) := mkApp5 (mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅
 def mkApp10 (f a b c d e₁ e₂ e₃ e₄ e₅ e₆ : Expr) := mkApp6 (mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅ e₆
 
-def mkCAppB (n : Name) (a b : Expr) := mkAppB (mkConst n) a b
 def mkDecIsTrue (pred proof : Expr) :=
 mkAppB (mkConst `Decidable.isTrue) pred proof
 
diff --git a/src/Init/Lean/Meta/Offset.lean b/src/Init/Lean/Meta/Offset.lean
index 31b028a1e2..1e2df634d3 100644
--- a/src/Init/Lean/Meta/Offset.lean
+++ b/src/Init/Lean/Meta/Offset.lean
@@ -95,8 +95,8 @@ match isOffset s with
 | some (s, k₁) => match isOffset t with
   | some (t, k₂) => -- s+k₁ =?= t+k₂
     if k₁ == k₂ then isDefEq s t
-    else if k₁ < k₂ then isDefEq s (mkCAppB `Nat.add t (mkNatLit $ k₂ - k₁))
-    else isDefEq (mkCAppB `Nat.add s (mkNatLit $ k₁ - k₂)) t
+    else if k₁ < k₂ then isDefEq s (mkAppB (mkConst `Nat.add) t (mkNatLit $ k₂ - k₁))
+    else isDefEq (mkAppB (mkConst `Nat.add) s (mkNatLit $ k₁ - k₂)) t
   | none => match evalNat t  with
     | some v₂ => -- s+k₁ =?= v₂
       if v₂ ≥ k₁ then isDefEq s (mkNatLit $ v₂ - k₁) else pure LBool.false
diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index a3e5a6efe5..1b32c4940a 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1443,7 +1443,7 @@ do tables ← tablesRef.get;
 def declareBuiltinParser (env : Environment) (addFnName : Name) (refDeclName : Name) (declName : Name) : IO Environment :=
 let name := `_regBuiltinParser ++ declName;
 let type := mkApp (mkConst `IO) (mkConst `Unit);
-let val  := mkCAppN addFnName #[mkConst refDeclName, toExpr declName, mkConst declName];
+let val  := mkAppN (mkConst addFnName) #[mkConst refDeclName, toExpr declName, mkConst declName];
 let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
 match env.addAndCompile {} decl with
 -- TODO: pretty print error
diff --git a/src/Init/Lean/ToExpr.lean b/src/Init/Lean/ToExpr.lean
index 1743884798..77c9fcc662 100644
--- a/src/Init/Lean/ToExpr.lean
+++ b/src/Init/Lean/ToExpr.lean
@@ -22,8 +22,8 @@ instance strToExpr : ToExpr String := ⟨mkStrLit⟩
 
 def nameToExprAux : Name → Expr
 | Name.anonymous  => mkConst `Lean.Name.anonymous
-| Name.str p s _  => mkCAppB `Lean.mkNameStr (nameToExprAux p) (toExpr s)
-| Name.num p n _  => mkCAppB `Lean.mkNameNum (nameToExprAux p) (toExpr n)
+| Name.str p s _  => mkAppB (mkConst `Lean.mkNameStr) (nameToExprAux p) (toExpr s)
+| Name.num p n _  => mkAppB (mkConst `Lean.mkNameNum) (nameToExprAux p) (toExpr n)
 
 instance nameToExpr : ToExpr Name := ⟨nameToExprAux⟩