diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index f95a0c43bb0aa00a748eee704597bac7fc55802e..6c757cda15b5618d123cc3069a038b38eae3832f 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -80,7 +80,8 @@ Definition complete : val :=
     let: "n1"  := Snd (Fst (Fst ("data"))) in
     let: "n2"  := Snd (Fst ("data")) in
     let: "p"   := Snd ("data") in
-    (* Create a thread identifier using NewProph. *)
+    (* Create a thread identifier using NewProph.
+    We don't actually need a prophecy ID here, just some unique identifier. *)
     let: "tid_ghost" := NewProph in
     let: "n_new" := (if: !"l_m" = "m1" then "n2" else "n1") in
     Resolve (CmpXchg "l_n" (InjR "l_descr") (InjL "n_new")) "p" "tid_ghost";;