follow recent changes of Sledgehammer defaults, as 0a46b3dbd5ad exposes a hint in the source text;