3 begin

     3 begin

     4 

     4 

     5 atom_decl name

     5 atom_decl name

     6 

     6 

     7 ML {* val _ = cheat_supp_eq := true *}

     7 ML {* val _ = cheat_supp_eq := true *}

     8 

     9 

     9 nominal_datatype lam =

    10 nominal_datatype lam =

    10   Var "name"

    11   Var "name"

    11 | App "lam" "lam"

    12 | App "lam" "lam"

    12 | Lam x::"name" t::"lam"  bind_set x in t

    13 | Lam x::"name" t::"lam"  bind_set x in t