[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"
begin

atom_decl name

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

end
"

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.