Previously, http://code.google.com/p/agda/issues/detail?id=64 has been simply an annoying infelicity... but with C-c C-c, it becomes a bug: printing names as if they are not in scope when they are does not produce valid code. (It wouldn't produce valid code if the names were actually out of scope, either, but that can't be helped ;-)