diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index b71187408a093ed2e2b9c3c823d68e413111cb90..31ead251dbcb14e5a00811a67dd84fe604fadf9e 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2237,9 +2237,6 @@ class cil_printer () = object (self)
            not state.print_cil_as_is &&
            not (Kernel.is_debug_key_enabled Kernel.dkey_print_bitfields) ->
          false
-       | "noreturn", [ ACons ("c11",[]) ]
-         when not state.print_cil_as_is ->
-         fprintf fmt "_Noreturn"; false
        | _ -> (* This is the default case *)
          (* Add underscores to the name *)
          let an' =