From 7e5fb3e493b239caa48fe6423be1aaa3ad811a8e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Feb 2015 11:35:01 -0800
Subject: [PATCH] fix(library/algebra/function): remove notation that conflicts
 with top-level notation for dependent pairs

---
 library/algebra/function.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/library/algebra/function.lean b/library/algebra/function.lean
index 4bb598290d..8649d51008 100644
--- a/library/algebra/function.lean
+++ b/library/algebra/function.lean
@@ -45,7 +45,5 @@ infixr  ∘'                 := dcompose
 infixl  on                 := on_fun
 infixr  $                  := app
 notation f `-[` op `]-` g  := combine f op g
--- Trick for using any binary function as infix operator
-notation a `⟨` f `⟩` b     :=  f a b
 
 end function