HomeIsabelle/Phabricator

Fix bug found by Makarius in generated code. It seems to have been introduced…

Authored by dcjm on Feb 27 2020, 7:41 PM.

Description

Fix bug found by Makarius in generated code. It seems to have been introduced in commit 19d82db2c when single RecDecs nodes were converted to Declar. That has been changed to keep them as RecDecs.