theory Ex1rec
imports "../Parser" 
begin

atom_decl name

ML {* val _ = recursive := true *}
ML {* val _ = alpha_type := AlphaGen *}
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