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