# HG changeset patch
# User blanchet
# Date 1367512476 -7200
# Node ID 6d756057e73688c036d4d5d2d17f8c8238d4cc00
# Parent  142a828838310c7249d63fc7174b3514d7708483
signature tuning

diff -r 142a82883831 -r 6d756057e736 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 18:25:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 18:34:36 2013 +0200
@@ -50,16 +50,16 @@
     * (thm list list * thm list list * Args.src list)
     * (thm list list * thm list list * Args.src list)
 
-  val co_datatypes: bool -> (mixfix list -> binding list -> binding list -> binding list ->
-      binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+  val co_datatypes: bool -> (mixfix list -> binding list -> binding list -> binding list list ->
+      binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
       local_theory -> BNF_FP_Util.fp_result * local_theory) ->
     (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
       ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
         mixfix) list) list ->
     local_theory -> local_theory
-  val parse_co_datatype_cmd: bool -> (mixfix list -> binding list -> binding list -> binding list ->
-      binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
-      local_theory -> BNF_FP_Util.fp_result * local_theory) ->
+  val parse_co_datatype_cmd: bool -> (mixfix list -> binding list -> binding list ->
+      binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
+      BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
     (local_theory -> local_theory) parser
 end;
 
@@ -912,8 +912,8 @@
            folds = fp_folds0, recs = fp_recs0, induct = fp_induct, strong_induct = fp_strong_induct,
            dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, set_thmss = fp_set_thmss,
            rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms, ...}, lthy)) =
-      fp_bnf construct_fp fp_bs mixfixes map_bs rel_bs set_bss (map dest_TFree unsorted_As) fp_eqs
-        no_defs_lthy0;
+      fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs mixfixes map_bs rel_bs set_bss
+        (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
 
     val timer = time (Timer.startRealTimer ());
 
diff -r 142a82883831 -r 6d756057e736 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 18:25:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 18:34:36 2013 +0200
@@ -165,8 +165,8 @@
 
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
 
-  val fp_bnf: (mixfix list -> binding list -> binding list -> binding list -> binding list list ->
-      (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> 'a) ->
+  val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
+    BNF_Def.bnf list -> local_theory -> 'a) ->
     binding list -> mixfix list -> binding list -> binding list -> binding list list ->
     (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.bnf list * 'a
 end;
@@ -491,7 +491,7 @@
 
     val timer = time (timer "Normalization & sealing of BNFs");
 
-    val res = construct_fp resBs (map TFree resDs, deadss) pre_bnfs lthy'';
+    val res = construct_fp bs resBs (map TFree resDs, deadss) pre_bnfs lthy'';
 
     val timer = time (timer "FP construction in total");
   in
@@ -508,8 +508,7 @@
       (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
         (empty_unfolds, lthy));
   in
-    mk_fp_bnf timer (construct_fp mixfixes bs map_bs rel_bs set_bss) resBs bs sort lhss bnfs Dss Ass
-      unfold_set lthy'
+    mk_fp_bnf timer construct_fp resBs bs sort lhss bnfs Dss Ass unfold_set lthy'
   end;
 
 end;
diff -r 142a82883831 -r 6d756057e736 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 18:25:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 18:34:36 2013 +0200
@@ -9,8 +9,8 @@
 
 signature BNF_GFP =
 sig
-  val construct_gfp: mixfix list -> binding list -> binding list -> binding list ->
-    binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+  val construct_gfp: mixfix list -> binding list -> binding list -> binding list list ->
+    binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
     local_theory -> BNF_FP_Util.fp_result * local_theory
 end;
 
@@ -55,7 +55,7 @@
      ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
 
 (*all BNFs have the same lives*)
-fun construct_gfp mixfixes bs map_bs rel_bs set_bss resBs (resDs, Dss) bnfs lthy =
+fun construct_gfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
 
diff -r 142a82883831 -r 6d756057e736 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 18:25:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 18:34:36 2013 +0200
@@ -8,8 +8,8 @@
 
 signature BNF_LFP =
 sig
-  val construct_lfp: mixfix list -> binding list -> binding list -> binding list ->
-    binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+  val construct_lfp: mixfix list -> binding list -> binding list -> binding list list ->
+    binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
     local_theory -> BNF_FP_Util.fp_result * local_theory
 end;
 
@@ -26,7 +26,7 @@
 open BNF_LFP_Tactics
 
 (*all BNFs have the same lives*)
-fun construct_lfp mixfixes bs map_bs rel_bs set_bss resBs (resDs, Dss) bnfs lthy =
+fun construct_lfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());