name-replace and name-replace* silently fail when a name cannot be used

[BenHocking]

When using name-replace (or name-replace*), if a name cannot be used then no message is provided to inform the user.

As an example of why this is important. I recently had a proof that was previously working fail after importing closest_approach_2D from vectors in the NASA library. The proof failed because after the import a renaming that used names x1, x2, y1, and y2 only used the y1 and y2 names, leaving the expressions to be renamed x1 and x2 alone. Those names were invalid because vectors@closest_approach_2D imported reals@quad_minmax, which imported reals@quadratic, which defined x1 and x2 as macros (which doesn't seem like a great idea to me, but that's another story, see issue #84).

Ideally, when this strategy failed, I would have been told that the strategy was not entirely successful and then told where the name conflict came from.

NB: the newly imported closest_approach_2D was added to help me with a completely different lemma, so it potentially could've been a long time between when I added that import and when I detected that my previously working proof was no longer working. Luckily, it was close enough in time that my first thought was to comment out that import to determine it was the culprit.