# HG changeset patch
# User blanchet
# Date 1367511388 -7200
# Node ID 55099e63c5ca59a746e75acdec14041ff7d6f1cd
# Parent  9761deff11bc50b3b706c6c08b38112af94c225e
tuned signature

diff -r 9761deff11bc -r 55099e63c5ca src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 16:33:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 18:16:28 2013 +0200
@@ -50,18 +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 -> (string * sort) list option -> binding list -> binding list -> binding list ->
-      binding list list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory ->
-      BNF_FP_Util.fp_result * local_theory) ->
+  val co_datatypes: bool -> (mixfix list -> binding list -> binding list -> binding list ->
+      binding list list -> (string * sort) list option -> 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 -> (string * sort) list option -> binding list -> binding list -> binding list ->
-      binding list 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 ->
+      binding list list -> (string * sort) list option -> typ list * typ list list ->
+      BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
     (local_theory -> local_theory) parser
 end;
 
diff -r 9761deff11bc -r 55099e63c5ca src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 16:33:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 18:16:28 2013 +0200
@@ -165,9 +165,9 @@
 
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
 
-  val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> binding list ->
-      binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list ->
-      local_theory -> 'a) ->
+  val fp_bnf: (mixfix list -> binding list -> binding list -> binding list -> binding list list ->
+      (string * sort) list option -> 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;
@@ -489,17 +489,17 @@
 
     val Dss = map3 (append oo map o nth) livess kill_poss deadss;
 
-    val ((bnfs'', deadss), lthy'') =
+    val ((pre_bnfs, deadss), lthy'') =
       fold_map3 (seal_bnf unfold_set') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy'
       |>> split_list;
 
     val timer = time (timer "Normalization & sealing of BNFs");
 
-    val res = construct_fp resBs bs map_bs rel_bs set_bss (map TFree resDs, deadss) bnfs'' lthy'';
+    val res = construct_fp bs map_bs rel_bs set_bss resBs (map TFree resDs, deadss) pre_bnfs lthy'';
 
     val timer = time (timer "FP construction in total");
   in
-    timer; (bnfs'', res)
+    timer; (pre_bnfs, res)
   end;
 
 fun fp_bnf construct_fp bs mixfixes map_bs rel_bs set_bss resBs eqs lthy =
diff -r 9761deff11bc -r 55099e63c5ca src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 16:33:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 18:16:28 2013 +0200
@@ -9,9 +9,9 @@
 
 signature BNF_GFP =
 sig
-  val construct_gfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
-    binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list ->
-    local_theory -> BNF_FP_Util.fp_result * local_theory
+  val construct_gfp: mixfix list -> binding list -> binding list -> binding list ->
+    binding list list -> (string * sort) list option -> typ list * typ list list ->
+    BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory
 end;
 
 structure BNF_GFP : BNF_GFP =
@@ -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 resBs bs map_bs rel_bs set_bss (resDs, Dss) bnfs lthy =
+fun construct_gfp mixfixes bs map_bs rel_bs set_bss resBs (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
 
diff -r 9761deff11bc -r 55099e63c5ca src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 16:33:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 18:16:28 2013 +0200
@@ -8,9 +8,9 @@
 
 signature BNF_LFP =
 sig
-  val construct_lfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
-    binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list ->
-    local_theory -> BNF_FP_Util.fp_result * local_theory
+  val construct_lfp: mixfix list -> binding list -> binding list -> binding list ->
+    binding list list -> (string * sort) list option -> typ list * typ list list ->
+    BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory
 end;
 
 structure BNF_LFP : BNF_LFP =
@@ -26,7 +26,7 @@
 open BNF_LFP_Tactics
 
 (*all BNFs have the same lives*)
-fun construct_lfp mixfixes resBs bs map_bs rel_bs set_bss (resDs, Dss) bnfs lthy =
+fun construct_lfp mixfixes bs map_bs rel_bs set_bss resBs (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());