5 text {* example 1, equivalent to example 2 from Terms *}

     5 text {* example 1, equivalent to example 2 from Terms *}

     6 

     6 

     7 atom_decl name

     7 atom_decl name

     8 

     8 

     9 ML {* val cheat_alpha_eqvt = ref false *}

     9 ML {* val cheat_alpha_eqvt = ref false *}

    10 

    11 

    11 nominal_datatype lam =

    12 nominal_datatype lam =

    12   VAR "name"

    13   VAR "name"

    13 | APP "lam" "lam"

    14 | APP "lam" "lam"

    14 | LET bp::"bp" t::"lam"   bind "bi bp" in t

    15 | LET bp::"bp" t::"lam"   bind "bi bp" in t