diff --git a/ProofMode.md b/ProofMode.md
index d86362ea802b50ebdf9abede793f4a7d2117c4cb..834e8ef3b8151fa51558c87827475cdaf08c8457 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -122,7 +122,7 @@ appear at the top level:
 - `>` : introduce a later (which strips laters from all hypotheses).
 - `{H1 ... Hn}` : clear `H1 ... Hn`.
 - `{$H1 ... $Hn}` : frame `H1 ... Hn` (this pattern can be mixed with the
-  previous pattern, e.g., `{$H1 H2 #H3}`).
+  previous pattern, e.g., `{$H1 H2 $H3}`).
 - `/=` : perform `simpl`.
 - `*` : introduce all universal quantifiers.
 - `**` : introduce all universal quantifiers, as well as all arrows and wands.