diff --git a/library/data/real/order.lean b/library/data/real/order.lean
index 627b32483..7dbddd440 100644
--- a/library/data/real/order.lean
+++ b/library/data/real/order.lean
@@ -15,7 +15,7 @@ open -[coercions] nat
 open eq eq.ops pnat
 local notation 0 := rat.of_num 0
 local notation 1 := rat.of_num 1
-notation 2 := subtype.tag (of_num 2) dec_trivial
+local notation 2 := subtype.tag (of_num 2) dec_trivial
 
 ----------------------------------------------------------------------------------------------------