I followed your advice and manually named all data. Here is what I found:
1. The inefficient data is in locale.ML, namely: structure Thms. Sets of theorems are represented as lists there. Changing this to Thmtab.set, and doing a pointer_eq test on merge seems to solve my performance issue.
2. Whether position information is displayed or not seems to depend on how the structure is actually generated, ie.
via. Theory_Data’, Theory_Data, or Generic_Data and also how the arguments are declared. Some observations:
* Theory_Data’ seems to result in a filename as position
* Generic_Data(struct Type T = … end) seems to result in a link as position
* Generic_Data(Type T = …) (without the explicit struct) seems to have no position information.
Norbert Schirmer (nschirmer at apple.com)
SEG Formal Verification