diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 6577161501..94e22f3341 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -380,15 +380,17 @@ def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
 @[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>
   withAttrKindGlobal stx fun stx => do
     match stx with
-    | `(infix $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
-      `(infixl $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f)
-    | `(infixr $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
-      `(notation $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? lhs $op:strLit rhs $[: $prec]? => $f lhs rhs)
     | `(infixl $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
-       let prec1 := quote <| (← evalOptPrec prec) + 1
-       `(notation $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? lhs $op:strLit rhs:$prec1 => $f lhs rhs)
+      let prec1 := quote <| (← evalOptPrec prec) + 1
+      `(notation $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? lhs$[:$prec]? $op:strLit rhs:$prec1 => $f lhs rhs)
+    | `(infix $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
+      let prec1 := quote <| (← evalOptPrec prec) + 1
+      `(notation $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? lhs:$prec1 $op:strLit rhs:$prec1 => $f lhs rhs)
+    | `(infixr $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
+      let prec1 := quote <| (← evalOptPrec prec) + 1
+      `(notation $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? lhs:$prec1 $op:strLit rhs $[: $prec]? => $f lhs rhs)
     | `(prefix $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
-       `(notation $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op:strLit arg $[: $prec]? => $f arg)
+      `(notation $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op:strLit arg $[: $prec]? => $f arg)
     | `(postfix $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
       `(notation $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? arg $op:strLit => $f arg)
     | _ => Macro.throwUnsupported
diff --git a/tests/lean/run/balg.lean b/tests/lean/run/balg.lean
index 20efabee49..5222c35eb3 100644
--- a/tests/lean/run/balg.lean
+++ b/tests/lean/run/balg.lean
@@ -14,7 +14,7 @@ abbrev mul {M : Magma} (a b : M) : M :=
 
 set_option pp.all true
 
-infix:70 (priority := high) "*" => mul
+infixl:70 (priority := high) "*" => mul
 
 structure Semigroup extends Magma where
   mul_assoc (a b c : α) : a * b * c = a * (b * c)