2 imports "../Nominal-General/Nominal2_Atoms"

     2 imports "../Nominal-General/Nominal2_Atoms"

     3         "../Nominal-General/Nominal2_Eqvt"

     3         "../Nominal-General/Nominal2_Eqvt"

     4         "../Nominal-General/Nominal2_Supp"

     4         "../Nominal-General/Nominal2_Supp"

     5         "Abs" "Perm" "Rsp"

     5         "Abs" "Perm" "Rsp"

     6 begin

     6 begin

     8 

     7 

     9 ML {*

     8 ML {*

    10 fun define_quotient_types binds tys alphas equivps ctxt =

     9 fun define_quotient_types binds tys alphas equivps ctxt =

    11 let

    10 let

    12   fun def_ty ((b, ty), (alpha, equivp)) ctxt =

    11   fun def_ty ((b, ty), (alpha, equivp)) ctxt =