diff --git a/ProofMode.md b/ProofMode.md
index b17ec1fc6073504b0a7dacda23631836ba789847..3e3f9c429863c8509a3faf057c5c81a2cb103330 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -18,8 +18,7 @@ Applying hypotheses and lemmas
   proof mode terms below.
   If the applied term has more premises than given specialization patterns, the
   pattern is extended with `[] ... []`.  As a consequence, all unused spatial
-  hypotheses move to the last premise without an explicit specialization
-  pattern.
+  hypotheses move to the last premise.
 
 Context management
 ------------------