diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index bd9aa5ba9a..9edca4e6fc 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -137,15 +137,9 @@ 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 := high) ppGroup(ppDedent("if " ident " : " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
+syntax (name := termDepIfThenElse) (priority := low) ppGroup(ppDedent("if " ident " : " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
 
-macro_rules
-  | `(if $h:ident : $c then $t:term else $e:term) => ``(dite $c (fun $h:ident => $t) (fun $h:ident => $e))
-
-syntax (name := termIfThenElse) (priority := high) ppGroup(ppDedent("if " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
-
-macro_rules
-  | `(if $c then $t:term else $e:term) => ``(ite $c $t $e)
+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)