moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
theory Term8
imports "../NewParser"
begin
(* example 8 *)
atom_decl name
(* this should work but gives an error at the moment:
in alpha_bn_rsp proof.
*)
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}"
end