diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 59ec1465a6d3c79a33e499c207b180ee66b1e853..d10a972435e8ed7c85c1a17a24a7063cabb66a11 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1320,7 +1320,7 @@ annotation:
                             "Only one code annotation is allowed per comment"))
       }
 | identifier { Aattribute_annot (loc $sloc, $1) }
-| BSGHOST { Aattribute_annot(loc(),"\\ghost") }
+| BSGHOST { Aattribute_annot(loc $sloc,"\\ghost") }
 ;
 
 contract_or_code_annotation: