The rename was done with the following command: $ sed -i 's/random_group_element_/random_ge_/g' $(git grep -l random_group_element_)
The rename was done with the following command: $ sed -i 's/random_group_element_/random_ge_/g' $(git grep -l random_group_element_)