Link to Definition.new_type_definition is missing from HTML index of symbolic identifiers

[ptroja]

The link to documentation of Definition.new_type_definition is not included in (automatically generated) help/src-sml/htmlsigs/idIndex.html.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[mn200]

Hmm. This is because there is no longer a separate Definition module. Rather, it's a sub-structure of Theory. There is good documentation of new_type_definition though, and it's a shame to lose the link to it. We'll have to think about that one.