remove Random.defaultRNG() (#25650)

Commit

7 years ago

remove Random.defaultRNG() (#25650) This function is an artifact of an intermediate state of PR #24874, but is not needed anymore.