diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 21f6a41f7d..916ec8d782 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -83,8 +83,8 @@ macro "∃" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Exis
 macro "exists" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Exists xs b
 macro "Σ" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Sigma xs b
 macro "Σ'" xs:explicitBinders ", " b:term : term => expandExplicitBinders `PSigma xs b
-macro:25 xs:bracketedExplicitBinders "×" b:term : term => expandBrackedBinders `Sigma xs b
-macro:25 xs:bracketedExplicitBinders "×'" b:term : term => expandBrackedBinders `PSigma xs b
+macro:35 xs:bracketedExplicitBinders "×" b:term:35  : term => expandBrackedBinders `Sigma xs b
+macro:35 xs:bracketedExplicitBinders "×'" b:term:35 : term => expandBrackedBinders `PSigma xs b
 
 syntax "funext " (colGt term:max)+ : tactic
 
diff --git a/tests/lean/run/sigmaprec.lean b/tests/lean/run/sigmaprec.lean
new file mode 100644
index 0000000000..45f3db8fb7
--- /dev/null
+++ b/tests/lean/run/sigmaprec.lean
@@ -0,0 +1,8 @@
+def f1 : Nat × Bool → Nat
+  | _ => 0
+
+def f2 : (α : Type) × α × α → Nat
+  | _ => 0
+
+def f3 : (x : Nat) × Bool → Nat
+  | _ => 0