--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Apr 09 13:15:21 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Apr 09 18:22:11 2014 +0200
@@ -7,9 +7,10 @@
signature BNF_FP_N2M =
sig
- val construct_mutualized_fp: BNF_Util.fp_kind -> typ list -> BNF_FP_Def_Sugar.fp_sugar list ->
- binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
- BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory
+ val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list ->
+ BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list ->
+ typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
+ BNF_FP_Util.fp_result * local_theory
end;
structure BNF_FP_N2M : BNF_FP_N2M =
@@ -46,7 +47,7 @@
Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
end;
-fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
+fun construct_mutualized_fp fp cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
(absT_infos : absT_info list) lthy =
let
fun of_fp_res get =