diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 8504c92965be7222fce1e7162a199f067c86912c..bfedc069ffcd735d1d32983da991d44fa8b1a3d4 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -17,7 +17,7 @@ of a location [l], this mechanism allows one to attach "meta" or "ghost" data to
 locations. This is done as follows:
 
 - When one allocates a location, in addition to the point-to connective [l ↦ v],
-  one also obtains the token [meta_token ⊤ l]. This token is an exclusive
+  one also obtains the token [meta_token l ⊤]. This token is an exclusive
   resource that denotes that no meta data has been associated with the
   namespaces in the mask [⊤] for the location [l].
 - Meta data tokens can be split w.r.t. namespace masks, i.e.