src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

     Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> (thm list -> thm list) ->
     local_theory -> gfp_sugar_thms
   val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
       binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
-    (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
-      ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
+    (bool * (bool * bool)) * (((((binding * (typ * sort)) list * binding) * (binding * binding))
+      * mixfix) * ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
         mixfix) list) list ->
     local_theory -> local_theory
   val parse_co_datatype_cmd: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
       binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->

      (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
      (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs))
   end;
 
 fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
-    (wrap_opts as (no_discs_sels, rep_compat), specs) no_defs_lthy0 =
+    (wrap_opts as (no_discs_sels, (_, rep_compat)), specs) no_defs_lthy0 =
   let
     (* TODO: sanity checks on arguments *)
 
     val _ = if fp = Greatest_FP andalso no_discs_sels then
         error "Cannot define codatatypes without discriminators and selectors"