diff --git a/src/library/hop_match.h b/src/library/hop_match.h
index ada6a9b399..089aac17cd 100644
--- a/src/library/hop_match.h
+++ b/src/library/hop_match.h
@@ -21,7 +21,7 @@ namespace lean {
    We say non-free variables occurring in \c p and \c t are "locally bound".
 
    \c p is a higher-order pattern when in all applications in \c p
-      1- A free variable is to the function OR
+      1- A free variable is not the function OR
       2- A free variable is the function, but all other arguments are distinct locally bound variables.
 
    \pre \c subst must be big enough to store all free variables occurring in subst