diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda
index 2671e6241a..dab8ab2505 100644
--- a/src/Reflection/AST/Definition.agda
+++ b/src/Reflection/AST/Definition.agda
@@ -68,8 +68,6 @@ constructor′-injective = < constructor′-injective₁ , constructor′-inject
 
 infix 4 _≟_
 
-infix 4 _≟_
-
 _≟_ : DecidableEquality Definition
 function cs       ≟ function cs′        =
   map′ (cong function) function-injective (cs Term.≟-Clauses cs′)