diff --git a/examples/linked_list_rev.mlw b/examples/linked_list_rev.mlw
index f28dce2ae2ceb348ff965c698ab17e01771b279e..8b43a13b9a0cd059d59e6677d0b6d76da637fc57 100644
--- a/examples/linked_list_rev.mlw
+++ b/examples/linked_list_rev.mlw
@@ -70,14 +70,14 @@ module InPlaceRev
 
   val next : ref (map loc loc)
 
-  let in_place_reverse (l:loc) (lM:list loc) : loc
+  let in_place_reverse (l:loc) (ghost lM:list loc) : loc
     requires { list_seg l !next lM null }
     ensures  { list_seg result !next (reverse lM) null }
   = 'Init:
     let p = ref l in
-    let pM = ref lM in
+    let ghost pM = ref lM in
     let r = ref null in
-    let rM = ref (Nil : list loc) in
+    let ghost rM = ref (Nil : list loc) in
     while !p <> null do
       invariant { list_seg !p !next !pM null }
       invariant { list_seg !r !next !rM null }