Assertion Fails in unusedby-proofs-of-formulas

[dMaggot]

In the presence of a datatype declaration in the root theory (argument theoryref in the unusedby-proofs-of-formulas LISP function) the assertion (assert th) in the unused-by-proofs-of LISP function fails. An simple way to reproduce is to add the following to Examples/sum.pvs

dummy_dt: DATATYPE
BEGIN
 dummy: dummy?
END dummy_dt

then open this theory in emacs and run

M-x tcp
M-x unsedby-proofs-of-formulas
Formula: closed_form
Formula:
Root theory to use as context: (default: sum):

The assertion will show in the pvs buffer. Reproduced in PVS 6.0 with Allegro and PVS 7.0 (from git) with SBCL.