fun abbreviate pp tsig naming mode tags (c, raw_rhs) consts =

 fun abbreviate pp tsig naming mode tags (c, raw_rhs) consts =

   let

   let

     val cert_term = certify pp tsig false consts;

     val cert_term = certify pp tsig false consts;

     val expand_term = certify pp tsig true consts;

     val expand_term = certify pp tsig true consts;

     val rhs = raw_rhs

     val rhs = raw_rhs

       |> Term.map_types (Type.cert_typ tsig)

       |> Term.map_types (Type.cert_typ tsig)

       |> cert_term;

       |> cert_term;

     val T = Term.fastype_of rhs;

     val T = Term.fastype_of rhs;