dump-sequent does not produce the promised `th-<theory name>.sequent` file

I'm chasing the cause of some proofs being tagged `incomplete`. Issuing `M-x dump-sequent` and answering `y` to the prompt doesn't produce a file (I can find). The only trace is in the buffer `pvs` which has these lines added:

```
sent:{(setq *dump-sequents-to-file* t)}

rec:{ 
t
pvs(51): }

rec:{nil
pvs(52): }
```