diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 1edc637e9..561e371de 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -156,7 +156,8 @@ theorem symm {A : TypeU} {a b : A} (H : a = b) : b = a
 theorem trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
 := subst H1 H2
 
-infixl 100 ⋈ : trans
+infixl 100 >< : trans
+infixl 100 ⋈  : trans
 
 theorem ne_symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a
 := assume H1 : b = a, H (symm H1)
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index b11d31aed..22631630e 100644
Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ