diff --git a/tests/lean/run/interp.lean b/tests/lean/run/interp.lean
index e2cd73a612..41e4a4e115 100644
--- a/tests/lean/run/interp.lean
+++ b/tests/lean/run/interp.lean
@@ -2,7 +2,7 @@ inductive Vector (α : Type u) : Nat → Type u
   | nil : Vector α 0
   | cons : α → Vector α n → Vector α (n+1)
 
-infix:67 (priority := high) " :: " => Vector.cons
+infix:67 " :: " => Vector.cons
 
 inductive Ty where
   | int