Reverted make-minus to earlier form
Added *record-undone-proofstate* and *all-rewrites-names* to the let in
prove-decl (formula-decl)
Mods from Cesar