monnier and leoliu Fix an obsolete form of with-demoted-errors and #' functions