[isabelle] the term export argument in `Assumption.export`



In `src/Pure/asssumption.ML`, the ML type `Assumption.export` is defined as `bool -> cterm list -> (thm -> thm) * (term -> term)`. The implementation documentation describes that as however of type `bool -> cterm list -> thm -> thm` (page 121 for version Isabelle2021), which loses the explanation about the second argument, the export map of type `term -> term`. I guess it is used for exporting some term shape, but what term it is, the term of proposition of the theorem or the term variables (fixed variables)? What it should be when I setting the assumption export?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.