1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Dec 02 20:31:54 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Dec 02 20:31:54 2013 +0100
     1.3 @@ -95,8 +95,8 @@
     1.4    val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
     1.5        binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
     1.6        BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
     1.7 -    (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
     1.8 -      ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
     1.9 +    (bool * (bool * bool)) * (((((binding * (typ * sort)) list * binding) * (binding * binding))
    1.10 +      * mixfix) * ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
    1.11          mixfix) list) list ->
    1.12      local_theory -> local_theory
    1.13    val parse_co_datatype_cmd: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    1.14 @@ -975,7 +975,7 @@
    1.15    end;
    1.16  
    1.17  fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
    1.18 -    (wrap_opts as (no_discs_sels, rep_compat), specs) no_defs_lthy0 =
    1.19 +    (wrap_opts as (no_discs_sels, (_, rep_compat)), specs) no_defs_lthy0 =
    1.20    let
    1.21      (* TODO: sanity checks on arguments *)
    1.22