[isabelle] Nominal2 Errors in simple datatype declarations

Hi, I'm getting some mysterious issues using the Nominal2 package. In the
following minimal example:

theory Test
imports Main "Nominal/Nominal2"

atom_decl name

nominal_datatype A = A "(name * B)"
and B = B nat


I get an "UnequalLengths" exception raised by line 544 of "library.ML"
which defines list zip ("~~"). Unfortunately, I don't know how to get stack
traces out of Isabelle theory runs. Any ideas on what's going on?

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