I totalled the numbers up again and the total was exactly £1.50 less than the total shown on the bill! My wife (having no faith in my basic adding skills) pulled out her phone telling me "don't be silly" and added them up to get the same result as I had.
We asked the waiter about it, who disappeared off to get his own calculator.. He added things up, looked confused and then took it off to the manager. She then repeated the process on the calculator and also looked confused, unable to explain what had happened. They gave us £1.50 in cash, apologised and then kept the receipt (I guess they didn't want us posting that on twitter!).
To this day I've no idea what happened. You could suggest that some programmer somewhere is getting rich off this, but it seems rather unlikely to me. I'd really love to know what the cause was (and whether the manager ever reported it further up the chain; because this seems like a rather serious error to me.. how often does it happen? is it always £1.50? did the issue get found/fixed?).