theory Term8imports "../NewParser"begin(* example 8 *)atom_decl name(* this should work but gives an error at the moment: seems like in the symmetry proof*)nominal_datatype foo = Foo0 "name"| Foo1 b::"bar" f::"foo" bind_set "bv b" in fand bar = Bar0 "name"| Bar1 "name" s::"name" b::"bar" bind s in bbinder bvwhere "bv (Bar0 x) = {}"| "bv (Bar1 v x b) = {atom v}"end