src/HOL/BNF/Tools/bnf_lfp.ML

 Datatype construction.
 *)
 
 signature BNF_LFP =
 sig
-  val construct_lfp: mixfix list -> (string * sort) list option -> binding list ->
+  val construct_lfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
     binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     BNF_FP.fp_result * local_theory
 end;
 
 structure BNF_LFP : BNF_LFP =

 open BNF_FP_Def_Sugar
 open BNF_LFP_Util
 open BNF_LFP_Tactics
 
 (*all BNFs have the same lives*)
-fun construct_lfp mixfixes resBs bs set_bss (resDs, Dss) bnfs lthy =
+fun construct_lfp mixfixes resBs bs map_bs set_bss (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
 
     val note_all = Config.get lthy bnf_note_all;
 

           end;
 
         fun wit_tac _ = mk_wit_tac n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Ibnfs, lthy) =
-          fold_map7 (fn tacs => fn b => fn set_bs => fn mapx => fn sets => fn T => fn wits =>
-              fn lthy =>
-            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) set_bs
+          fold_map8 (fn tacs => fn b => fn map_b => fn set_bs => fn mapx => fn sets => fn T =>
+              fn wits => fn lthy =>
+            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) map_b set_bs
               (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
             |> register_bnf (Local_Theory.full_name lthy b))
-          tacss bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
+          tacss bs map_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
 
         val fold_maps = fold_thms lthy (map (fn bnf =>
           mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Ibnfs);
 
         val fold_sets = fold_thms lthy (maps (fn bnf =>