default_random
Even if that variable is deprecated, it is still used internally by `get_default_random()`.