Re: [isabelle] Nominal2 Errors in simple datatype declarations

This is because you declare A to have a pair-type. It should

work if you say

  ... = A name B

and it should have the same effect, except that you do not


  A (x,b)


 A x b

Hope this helps,


PS: I am on vacation until next week...if more problems crop up,

I might not be very quick with responding, but I try to keep an

eye on my email.

From: Edward Pierzchalski <e.a.pierzchalski at>
Sent: 04 August 2016 09:28:23
To: cl-isabelle-users at; Urban, Christian
Subject: 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.