More informative message when Mltop.load_object fails.
Fixing the place where to insert a space in "Tactic failure"
message. Otherwise, a heading space was missing when calling tclFAIL
from ML tactics.
Making code and doc agree on "Set Equality Schemes" (see also bug #2550).