668 atom_decl name

   668 

   669 

   669 end

   670 nominal_datatype exp =

   670 

   671   EVar name

   671 

   672 | EUnit

   672 

   673 | EPair exp exp

   674 | ELetRec l::lrbs e::exp     bind "b_lrbs l" in e

   675 

   676 and fnclause =

   677   K x::name p::pat f::exp    bind "b_pat p" in f 

   678 

   679 and fnclauses =

   680   S fnclause

   681 | ORs fnclause fnclauses

   682 

   683 and lrb =

   684   Clause fnclauses

   685 

   686 and lrbs =

   687   Single lrb

   688 | More lrb lrbs

   689 

   690 and pat =

   691   PVar name

   692 | PUnit

   693 | PPair pat pat

   694 

   695 binder

   696   b_lrbs      :: "lrbs \<Rightarrow> atom set" and

   697   b_pat       :: "pat \<Rightarrow> atom set" and

   698   b_fnclauses :: "fnclauses \<Rightarrow> atom set" and

   699   b_fnclause  :: "fnclause \<Rightarrow> atom set" and

   700   b_lrb       :: "lrb \<Rightarrow> atom set"

   701 

   702 where

   703   "b_lrbs (Single l) = b_lrb l"

   704 | "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls"

   705 | "b_pat (PVar x) = {atom x}"

   706 | "b_pat (PUnit) = {}"

   707 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"

   708 | "b_fnclauses (S fc) = (b_fnclause fc)"

   709 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"

   710 | "b_lrb (Clause fcs) = (b_fnclauses fcs)"

   711 | "b_fnclause (K x pat exp) = {atom x}"

   712 

   713 

   714 end

   715 

   716 

   717