changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
theory Term8
imports "../NewParser"
begin
(* example 8 *)
atom_decl name
ML {* val _ = cheat_alpha_bn_rsp := true *}
nominal_datatype foo =
Foo0 "name"
| Foo1 b::"bar" f::"foo" bind_set "bv b" in f
and bar =
Bar0 "name"
| Bar1 "name" s::"name" b::"bar" bind_set s in b
binder
bv
where
"bv (Bar0 x) = {}"
| "bv (Bar1 v x b) = {atom v}"
thm foo_bar.supp
end