src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 56484 c451cf8b29c8
parent 55966 972f0aa7091b
child 56486 753b779d070d
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 09 13:15:21 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 09 18:22:11 2014 +0200
     1.3 @@ -7,9 +7,10 @@
     1.4  
     1.5  signature BNF_FP_N2M =
     1.6  sig
     1.7 -  val construct_mutualized_fp: BNF_Util.fp_kind -> typ list -> BNF_FP_Def_Sugar.fp_sugar list ->
     1.8 -    binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
     1.9 -    BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory
    1.10 +  val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list ->
    1.11 +    BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list ->
    1.12 +    typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
    1.13 +    BNF_FP_Util.fp_result * local_theory
    1.14  end;
    1.15  
    1.16  structure BNF_FP_N2M : BNF_FP_N2M =
    1.17 @@ -46,7 +47,7 @@
    1.18      Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
    1.19    end;
    1.20  
    1.21 -fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
    1.22 +fun construct_mutualized_fp fp cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
    1.23      (absT_infos : absT_info list) lthy =
    1.24    let
    1.25      fun of_fp_res get =