1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 18:25:44 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 18:34:36 2013 +0200
     1.3 @@ -50,16 +50,16 @@
     1.4      * (thm list list * thm list list * Args.src list)
     1.5      * (thm list list * thm list list * Args.src list)
     1.6  
     1.7 -  val co_datatypes: bool -> (mixfix list -> binding list -> binding list -> binding list ->
     1.8 -      binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
     1.9 +  val co_datatypes: bool -> (mixfix list -> binding list -> binding list -> binding list list ->
    1.10 +      binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    1.11        local_theory -> BNF_FP_Util.fp_result * local_theory) ->
    1.12      (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
    1.13        ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
    1.14          mixfix) list) list ->
    1.15      local_theory -> local_theory
    1.16 -  val parse_co_datatype_cmd: bool -> (mixfix list -> binding list -> binding list -> binding list ->
    1.17 -      binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    1.18 -      local_theory -> BNF_FP_Util.fp_result * local_theory) ->
    1.19 +  val parse_co_datatype_cmd: bool -> (mixfix list -> binding list -> binding list ->
    1.20 +      binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    1.21 +      BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
    1.22      (local_theory -> local_theory) parser
    1.23  end;
    1.24  
    1.25 @@ -912,8 +912,8 @@
    1.26             folds = fp_folds0, recs = fp_recs0, induct = fp_induct, strong_induct = fp_strong_induct,
    1.27             dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, set_thmss = fp_set_thmss,
    1.28             rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms, ...}, lthy)) =
    1.29 -      fp_bnf construct_fp fp_bs mixfixes map_bs rel_bs set_bss (map dest_TFree unsorted_As) fp_eqs
    1.30 -        no_defs_lthy0;
    1.31 +      fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs mixfixes map_bs rel_bs set_bss
    1.32 +        (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
    1.33  
    1.34      val timer = time (Timer.startRealTimer ());
    1.35  

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 18:25:44 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 18:34:36 2013 +0200
     2.3 @@ -165,8 +165,8 @@
     2.4  
     2.5    val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
     2.6  
     2.7 -  val fp_bnf: (mixfix list -> binding list -> binding list -> binding list -> binding list list ->
     2.8 -      (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> 'a) ->
     2.9 +  val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
    2.10 +    BNF_Def.bnf list -> local_theory -> 'a) ->
    2.11      binding list -> mixfix list -> binding list -> binding list -> binding list list ->
    2.12      (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.bnf list * 'a
    2.13  end;
    2.14 @@ -491,7 +491,7 @@
    2.15  
    2.16      val timer = time (timer "Normalization & sealing of BNFs");
    2.17  
    2.18 -    val res = construct_fp resBs (map TFree resDs, deadss) pre_bnfs lthy'';
    2.19 +    val res = construct_fp bs resBs (map TFree resDs, deadss) pre_bnfs lthy'';
    2.20  
    2.21      val timer = time (timer "FP construction in total");
    2.22    in
    2.23 @@ -508,8 +508,7 @@
    2.24        (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
    2.25          (empty_unfolds, lthy));
    2.26    in
    2.27 -    mk_fp_bnf timer (construct_fp mixfixes bs map_bs rel_bs set_bss) resBs bs sort lhss bnfs Dss Ass
    2.28 -      unfold_set lthy'
    2.29 +    mk_fp_bnf timer construct_fp resBs bs sort lhss bnfs Dss Ass unfold_set lthy'
    2.30    end;
    2.31  
    2.32  end;

     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 18:25:44 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 18:34:36 2013 +0200
     3.3 @@ -9,8 +9,8 @@
     3.4  
     3.5  signature BNF_GFP =
     3.6  sig
     3.7 -  val construct_gfp: mixfix list -> binding list -> binding list -> binding list ->
     3.8 -    binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
     3.9 +  val construct_gfp: mixfix list -> binding list -> binding list -> binding list list ->
    3.10 +    binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    3.11      local_theory -> BNF_FP_Util.fp_result * local_theory
    3.12  end;
    3.13  
    3.14 @@ -55,7 +55,7 @@
    3.15       ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
    3.16  
    3.17  (*all BNFs have the same lives*)
    3.18 -fun construct_gfp mixfixes bs map_bs rel_bs set_bss resBs (resDs, Dss) bnfs lthy =
    3.19 +fun construct_gfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy =
    3.20    let
    3.21      val timer = time (Timer.startRealTimer ());
    3.22  

     4.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 18:25:44 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 18:34:36 2013 +0200
     4.3 @@ -8,8 +8,8 @@
     4.4  
     4.5  signature BNF_LFP =
     4.6  sig
     4.7 -  val construct_lfp: mixfix list -> binding list -> binding list -> binding list ->
     4.8 -    binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
     4.9 +  val construct_lfp: mixfix list -> binding list -> binding list -> binding list list ->
    4.10 +    binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    4.11      local_theory -> BNF_FP_Util.fp_result * local_theory
    4.12  end;
    4.13  
    4.14 @@ -26,7 +26,7 @@
    4.15  open BNF_LFP_Tactics
    4.16  
    4.17  (*all BNFs have the same lives*)
    4.18 -fun construct_lfp mixfixes bs map_bs rel_bs set_bss resBs (resDs, Dss) bnfs lthy =
    4.19 +fun construct_lfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy =
    4.20    let
    4.21      val timer = time (Timer.startRealTimer ());
    4.22