diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 8c5800a88273fb117ae6f40db4e23ad3e2187258..61e3a74536f3c3ea45417d7a2c72231d4eecc40c 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -361,6 +361,8 @@ let rOP = [
 ]
 let comment_line = "//" [^'\n']*
 let rIdentifier = rL (rL | rD)*
+let xIdentifier = rL (rL | rD | "'")*
+let opIdentifier = (rL | rD | rOP)+
 
 (* Do not forget to update also the corresponding chr rule if you add
    a supported escape sequence here. *)
@@ -390,9 +392,8 @@ rule token = parse
      check_ext_plugin (fst cabsloc) plugin tok
      }
   | '\\' rIdentifier { bs_identifier lexbuf }
-  | rIdentifier ( "::" rIdentifier )+                 { longident lexbuf }
-  | rIdentifier ( "::" rIdentifier )+ "'" rIdentifier { longident lexbuf }
-  | rIdentifier ( "::" rIdentifier )* "::(" rOP+ ")"  { longident lexbuf }
+  | ( rIdentifier "::")+     xIdentifier      { longident lexbuf }
+  | ( rIdentifier "::")+ "(" opIdentifier ")" { longident lexbuf }
   | rIdentifier       {
       let loc = Lexing.(lexeme_start_p lexbuf, lexeme_end_p lexbuf) in
       let cabsloc = Cil_datatype.Location.of_lexing_loc loc in