diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index ccf88a9025fa45096c9c12ce0377091e11a40915..f56d457bb9e8f3cf0362593497797b9cd82a2cd3 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -866,6 +866,8 @@ let global_env = Datatype.String.Hashtbl.create 307
 (* ghost global environment: superset of global and subset of ghost *)
 let ghost_global_env = Datatype.String.Hashtbl.create 307
 
+(* maps a C label to the ghost environment of variables in scope
+   at this program point. Used for typing \at() terms and predicates. *)
 let label_env = Datatype.String.Hashtbl.create 307
 
 let add_label_env lab =
@@ -876,7 +878,7 @@ let add_label_env lab =
     | _ -> map
   in
   let open Datatype.String.Hashtbl in
-  let lab_env = fold add_if_absent env Datatype.String.Map.empty in
+  let lab_env = fold add_if_absent ghost_env Datatype.String.Map.empty in
   add label_env lab lab_env
 
 let remove_label_env lab =
diff --git a/tests/syntax/oracle/ghost_local_capture.res.oracle b/tests/syntax/oracle/ghost_local_capture.res.oracle
index 28e38a724bb6e303addb1d16bb2f7c6d1bcec896..dc24b079c5afc72e0080121870b5691f42fe3523 100644
--- a/tests/syntax/oracle/ghost_local_capture.res.oracle
+++ b/tests/syntax/oracle/ghost_local_capture.res.oracle
@@ -10,7 +10,7 @@ void titi(void)
     c = 2;
     /*@ assert c_0 ≡ 1; */ ;
     /*@ assert \at(c,L0) ≡ 0; */ ;
-    /*@ assert \at(c,L1) ≡ 1; */ ;
+    /*@ assert \at(c_0,L1) ≡ 1; */ ;
   }
   /*@ assert c ≡ 2; */ ;
   return;