4 

     5 atom_decl var

     6 

     7 ML {* trace := true *}

     8 declare [[ML_print_depth = 1000]]

     9 

    10 nominal_datatype exp =

    11           Var var

    12         | App exp var

    13         | LetA as::assn body::exp binds "bn as" in "body" "as"

    14         | Lam x::var body::exp binds x in body

    15         and assn =

    16           ANil | ACons var exp assn

    17         binder

    18           bn

    19         where "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)"

    20 

    21 nominal_datatype ('ann::fs) exp2 =

    22   Var var

    23 | App "'ann exp2" var

    24 | LetA as::"'ann assn2" body::"'ann exp2" binds "bnn as" in body as

    25 | Lam x::var body::"'ann exp2" binds x in body

    26 and ('ann::fs) assn2 =

    27   ANil 

    28 | ACons var "'ann exp2" 'ann "'ann assn2"

    29 binder

    30   bnn :: "('ann::fs) assn2 \<Rightarrow> atom list"

    31 where 

    32   "bnn ANil = []" 

    33 | "bnn (ACons x a t as) = (atom x) # (bnn as)"

    34