diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index a6d48ba6ba7f3faa2e06658ab02be4c4ee452e41..bc9017f7a08c6135c22fa01fbf9de0cc7ae2c2e7 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -76,9 +76,7 @@ let has_definition kf = match kf.fundec with
   | Definition  _ -> true
   | Declaration _ -> false
 
-let is_ghost kf = match kf.fundec with
-  | Definition ({ svar = { vghost }}, _)
-  | Declaration (_, { vghost },_, _) -> vghost
+let is_ghost kf = (get_vi kf).vghost
 
 (* ************************************************************************* *)
 (** {2 Kernel functions are comparable} *)