5 atom_decl name

     5 atom_decl name

     6 atom_decl ident

     6 atom_decl ident

     7 

     7 

     8 datatype rtrm2 =

     8 datatype rtrm2 =

     9   rVr2 "name"

     9   rVr2 "name"

    11 | rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)"

    11 | rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)"

    12 and ras =

    12 and ras =

    13   rAs "name" "rtrm2"

    13   rAs "name" "rtrm2"

    14 

    14 

    15 primrec rbv2 where "rbv2 (rAs x t) = {atom x}"

    15 primrec rbv2 where "rbv2 (rAs x t) = {atom x}"

    43 val ntnames = [(@{binding trm2}, @{typ rtrm2}), (@{binding as}, @{typ ras})]

    43 val ntnames = [(@{binding trm2}, @{typ rtrm2}), (@{binding as}, @{typ ras})]

    44 val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]], 

    44 val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]], 

    45              [[[], []]]  (*, [[], [[], []]] *) ];

    45              [[[], []]]  (*, [[], [[], []]] *) ];

    46 val bv_simps = @{thms rbv2.simps}

    46 val bv_simps = @{thms rbv2.simps}

    47 val info = Datatype.the_info @{theory} ftname;

    47 val info = Datatype.the_info @{theory} ftname;

    48 val descr = #descr info;

    52 val descr = #descr info;

    49 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;

    53 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;

    50 val full_tnames = List.take (all_full_tnames, length tnames);

    54 val full_tnames = List.take (all_full_tnames, length tnames);

    51 val induct = #induct info;

    55 val induct = #induct info;

    52 val inducts = #inducts info;

    56 val inducts = #inducts info;