failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is
s/\\([a-zA-Z]+)\s*/$1/g;
s/\$//g;
s/^BOOKMARK/\\BOOKMARK/g;