# [isabelle] Nominal2 and exception UnequalLengths raised

Hello,
I am attempting to define programming language case statements in Nominal2
and get
exception UnequalLengths raised (line 519 of "library.ML")
A possible workaround is to define case_branch to be list like and so avoid
"case_branch list":
case_branch =
B_nil | B_cons x::x s::stmt case_branch binds x in s
but this is a little messy.
A cut down version that exhibits the problem is:
theory Nominal2Exception
imports "Nominal2.Nominal2"
begin
atom_decl x
nominal_datatype expr =
E1 x
nominal_datatype stmt =
S1 "case_branch list"
| S2 expr
and case_branch =
B1 x::x s::stmt binds x in s
end
and the full text from the output window is:
Proofs for inductive predicate(s) "rep_set_stmt_raw_case_branch_raw_1",
"rep_set_stmt_raw_case_branch_raw_2", "rep_set_stmt_raw_case_branch_raw_3"
Proving monotonicity ...
Proving the introduction rules ...
Proving the induction rule ...
Proofs for inductive predicate(s) "rec_set_stmt_raw_case_branch_raw_1",
"rec_set_stmt_raw_case_branch_raw_2", "rec_set_stmt_raw_case_branch_raw_3"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the simplification rules ...
exception UnequalLengths raised (line 519 of "library.ML")

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