theory Ex1rec
imports "Parser" "../Attic/Prove"
begin

atom_decl name

ML {* val _ = recursive := true *}
nominal_datatype lam' =
  VAR' "name"
| APP' "lam'" "lam'"
| LAM' x::"name" t::"lam'"  bind x in t
| LET' bp::"bp'" t::"lam'"   bind "bi' bp" in t
and bp' =
  BP' "name" "lam'"
binder
  bi'::"bp' \<Rightarrow> atom set"
where
  "bi' (BP' x t) = {atom x}"

thm lam'_bp'.fv
thm lam'_bp'.eq_iff[no_vars]
thm lam'_bp'.bn
thm lam'_bp'.perm
thm lam'_bp'.induct
thm lam'_bp'.inducts
thm lam'_bp'.distinct
ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
thm lam'_bp'.fv[simplified lam'_bp'.supp]

end