diff --git a/src/parser/parser.mly b/src/parser/parser.mly
index 41d45be234f49f69b6f5d5cf7b86abe6f8eb6aae..bb861144f55154eafd30c76bd5d52e3084a0d7d8 100644
--- a/src/parser/parser.mly
+++ b/src/parser/parser.mly
@@ -995,6 +995,7 @@ uident_nq:
 
 lident:
 | LIDENT          { mk_id $1 $startpos $endpos }
+| lident_keyword  { mk_id $1 $startpos $endpos }
 | LIDENT_QUOTE    { mk_id $1 $startpos $endpos }
 
 lident_nq:
diff --git a/theories/map.why b/theories/map.why
index 55ebecfd9041cebb113700d6dfc397a0da5fb79e..31a95c28681c5c164d827c16b074247ba9a1122a 100644
--- a/theories/map.why
+++ b/theories/map.why
@@ -195,14 +195,14 @@ theory MapInjection
   (** [surjective a n] is true when [a] is a surjection
       from [(0..n-1)] to [(0..n-1)] *)
 
-  predicate range' (a: map int int) (n: int) =
+  predicate range (a: map int int) (n: int) =
     forall i: int. 0 <= i < n -> 0 <= a[i] < n
-  (** [range' a n] is true when [a] maps the domain
+  (** [range a n] is true when [a] maps the domain
       [(0..n-1)] into [(0..n-1)] *)
 
   lemma injective_surjective:
     forall a: map int int, n: int.
-    injective a n -> range' a n -> surjective a n
+    injective a n -> range a n -> surjective a n
   (** main lemma: an injection on [(0..n-1)] that
       ranges into [(0..n-1)] is also a surjection *)