70   fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];

    70   fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];

    71   fun mk_union sets =

    71   fun mk_union sets =

    72     fold (fn a => fn b =>

    72     fold (fn a => fn b =>

    73       if a = noatoms then b else

    73       if a = noatoms then b else

    74       if b = noatoms then a else

    74       if b = noatoms then a else

    75       HOLogic.mk_binop "Set.union" (a, b)) (rev sets) noatoms;

    76       HOLogic.mk_binop "Set.union" (a, b)) (rev sets) noatoms;

    76   fun mk_conjl props =

    77   fun mk_conjl props =

    77     fold (fn a => fn b =>

    78     fold (fn a => fn b =>

    78       if a = @{term True} then b else

    79       if a = @{term True} then b else

    79       if b = @{term True} then a else

    80       if b = @{term True} then a else

   122   val alpha_frees = map Free (alpha_names ~~ alpha_types);

   123   val alpha_frees = map Free (alpha_names ~~ alpha_types);

   123   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =

   124   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =

   124     let

   125     let

   125       val Ts = map (typ_of_dtyp descr sorts) dts;

   126       val Ts = map (typ_of_dtyp descr sorts) dts;

   126       val bindslen = length bindcs

   127       val bindslen = length bindcs

   128       val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs;

   130       val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs;

   129       val bind_pis = bindcs ~~ pis;

   131       val bind_pis = bindcs ~~ pis;

   130       val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts);

   132       val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts);

   131       val args = map Free (names ~~ Ts);

   133       val args = map Free (names ~~ Ts);

   132       val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts);

   134       val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts);