I'm not entirely clear what I should be doing. Should I rename the file myself, and verify that any mention of the file name in other source files and docs is also changed?
That would be great, yes. In SVN would be best.
What about other things, like the HaloMassFcn.py file? Does that need to be renamed?
I missed that one, but yes, because it defines a class name the same as the object name, it should be renamed. Perhaps halo_mass_function.py.