[isabelle] custom serialization for records

Dear Isabelle users,

When using the code generator, I need to map a record type to another record type definition.

I used the code_type to specify the record type mapping, and a code_const for each selector,
but the export_code command returned the following error:

exception Match raised (line 239 of "~~/src/Tools/Code/code_ml.ML")

Can anyone help me on this please?

Thanks in advance


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