5 text {* example 3 or example 5 from Terms.thy *}

     5 text {* example 3 or example 5 from Terms.thy *}

     6 

     6 

     7 atom_decl name

     7 atom_decl name

     8 

     8 

     9 ML {* val _ = recursive := false  *}

     9 ML {* val _ = recursive := false  *}

    10 nominal_datatype trm =

    12 nominal_datatype trm =

    11   Vr "name"

    13   Vr "name"

    12 | Ap "trm" "trm"

    14 | Ap "trm" "trm"

    13 | Lm x::"name" t::"trm"  bind x in t

    15 | Lm x::"name" t::"trm"  bind x in t

    14 | Lt a::"lts" t::"trm"   bind "bn a" in t

    16 | Lt a::"lts" t::"trm"   bind "bn a" in t