PHP 7 update introduces constant DATE_RFC7231

PHP 7.0.19 and PHP 7.1.5 update introduces constant DATE_RFC7231, which breaks existing Drupal 7 site with a message "DATE_RFC7231 already defined". This patch was proposed here: https://www.drupal.org/node/2877243

includes/bootstrap.inc

@@ -255,8 +255,13 @@ define('DRUPAL_PHP_FUNCTION_PATTERN', '[a-zA-Z_\x7f-\xff][a-zA-Z0-9_\x7f-\xff]*'
  *
  * Example: Sun, 06 Nov 1994 08:49:37 GMT
  */
-define('DATE_RFC7231', 'D, d M Y H:i:s \G\M\T');
 
+/** This constant was introduced in PHP 7.0.19 and PHP 7.1.5 but needs to be
+ * defined by Drupal for earlier PHP versions.
+ */
+if (!defined('DATE_RFC7231')) {
+  define('DATE_RFC7231', 'D, d M Y H:i:s \G\M\T');
+}
 /**
  * Provides a caching wrapper to be used in place of large array structures.
  *