1 theory Term8

     2 imports "../NewParser"

     3 begin

     4 

     5 (* example 8 from Terms.thy *)

     6 

     7 atom_decl name

     8 

     9 nominal_datatype foo =

    10   Foo0 "name"

    11 | Foo1 b::"bar" f::"foo" bind_set "bv b" in f

    12 and bar =

    13   Bar0 "name"

    14 | Bar1 "name" s::"name" b::"bar" bind_set s in b

    15 binder

    16   bv

    17 where

    18   "bv (Bar0 x) = {}"

    19 | "bv (Bar1 v x b) = {atom v}"

    20 

    21 end

    22 

    23