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.
Description
Description
Details
Details
- Provenance
dcjm Authored on Feb 27 2020, 7:41 PM - Parents
- rPOLYML5237b653aa69: Rename Root.ML to avoid possible conflict with ROOT.ML in Isabelle.
- Branches
- Unknown
- Tags
- Reverted By
- rPOLYMLfb10196d998b: Convert single bindings from mutual recursion into simple bindings.