shortcode gallery edit not showing

I’m editing the gallery_shortcode() function, but no matter what I do to it, it doesn’t change how I view the actual post.

Just now I’ve changed 'itemtag' => 'dl', to 'itemtag' => 'ol',. It’s still showing the <dl> on the post.

I’ve checked, and this is what the remote copy of the file wordpress/includes/media.php looks like. Do I have to edit something else for these changes to take place? (And yes, I’ve cleared my cache, but still no change.) Am I missing something?