They were insulted when I asked to measure the DC output: this had been their shop power supply for ten years !
It measured 50 volts DC. The autotransformer had slipped or shorted one winding, so it was nominally at 5:2 instead of at 5:1.
They should have a "Like" button on this forum for posts like this.