diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 9edca4e6fc..7d3fb4098e 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -137,10 +137,6 @@ infixr:100 " <$> " => Functor.map
 macro_rules | `($x <|> $y) => `(binop_lazy% HOrElse.hOrElse $x $y)
 macro_rules | `($x >> $y)  => `(binop_lazy% HAndThen.hAndThen $x $y)
 
-syntax (name := termDepIfThenElse) (priority := low) ppGroup(ppDedent("if " ident " : " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
-
-syntax (name := termIfThenElse) (priority := low) ppGroup(ppDedent("if " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
-
 macro "if " "let " pat:term " := " d:term " then " t:term " else " e:term : term =>
   `(match $d:term with | $pat:term => $t | _ => $e)
 
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 02471f84bd..8df13de2a6 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -64,25 +64,6 @@ open Meta
       `(dite $c (fun $h:ident => $t) (fun $h:ident => $e))
   withMacroExpansion stx newStx <| elabTerm newStx expectedType?
 
--- TODO: delete
-@[builtinTermElab termDepIfThenElse] def elabIfOld1 : TermElab := fun stx expectedType? => do
-  /- "if " ident " : " term " then" term "else" term -/
-  let h := stx[1]
-  let c := stx[3]
-  let t := stx[5]
-  let e := stx[7]
-  let newStx ← `(dite $c (fun $h:ident => $t) (fun $h:ident => $e))
-  withMacroExpansion stx newStx <| elabTerm newStx expectedType?
-
--- TODO: delete
-@[builtinTermElab termIfThenElse] def elabIfOld2 : TermElab := fun stx expectedType? => do
-  /- "if " term " then" term "else" term -/
-  let c := stx[1]
-  let t := stx[3]
-  let e := stx[5]
-  let newStx ← `(ite $c $t $e)
-  withMacroExpansion stx newStx <| elabTerm newStx expectedType?
-
 @[builtinTermElab borrowed] def elabBorrowed : TermElab := fun stx expectedType? =>
   match stx with
   | `(@& $e) => return markBorrowed (← elabTerm e expectedType?)