diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b7aead68ca96662941c7c92f8cf52d1f4b4b2aba..15077459b68c0a7c3925cce0c0be8cd002457b3d 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6298,7 +6298,7 @@ and doExp local_env
       end
     | Cabs.CALL({ expr_node = VARIABLE "__builtin_choose_expr"},
                 args, ghost_args)
-      when Cil.gccMode() ->
+      when Machine.gccMode() ->
       (* __builtin_choose_expr is supposed to choose at compile time between
          two expressions, hence we have to handle it separately from the
          normal calls. *)