# HG changeset patch
# User blanchet
# Date 1473249196 -7200
# Node ID 9cd3dabfeea8539b7578b6806ee9d29521922f81
# Parent  6d83841134f8d9067db5ec4df689de302401d522
exported ML functions + tuning

diff -r 6d83841134f8 -r 9cd3dabfeea8 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 07 13:53:16 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 07 13:53:16 2016 +0200
@@ -105,6 +105,21 @@
   val liveness_of_fp_bnf: int -> BNF_Def.bnf -> bool list
   val nesting_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
 
+  val define_ctrs_dtrs_for_type: string -> typ -> term -> term -> thm -> thm -> int -> int list ->
+    term -> binding list -> mixfix list -> typ list list -> local_theory ->
+    (term list list * term list * thm * thm list) * local_theory
+  val wrap_ctrs: BNF_Util.fp_kind -> (string -> bool) -> bool -> string -> thm -> int -> int list ->
+    thm -> thm -> binding list -> binding list list -> term list -> term list -> thm -> thm list ->
+    local_theory -> Ctr_Sugar.ctr_sugar * local_theory
+  val derive_map_set_rel_pred_thms: (string -> bool) -> BNF_Util.fp_kind -> int -> typ list ->
+    typ list -> typ -> typ -> thm list -> thm list -> thm list -> thm list -> thm list ->
+    thm list -> thm list -> thm list -> string -> BNF_Def.bnf -> BNF_Def.bnf list -> typ -> term ->
+    thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm -> typ list list -> term ->
+    Ctr_Sugar.ctr_sugar -> Proof.context ->
+    (thm list * thm list * thm list list * thm list * thm list * thm list * thm list * thm list
+     * thm list * thm list * thm list list list list * thm list list list list * thm list
+     * thm list * thm list * thm list * thm list) * local_theory
+
   type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list)
 
   val morph_lfp_sugar_thms: morphism -> lfp_sugar_thms -> lfp_sugar_thms
@@ -2345,7 +2360,6 @@
 
     val (xtor_co_recs, recs_args_types, corecs_args_types) =
       mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0;
-    val lthy' = lthy;
 
     fun define_ctrs_dtrs_for_type_etc fp_bnf fp_b fpT C E ctor dtor xtor_co_rec ctor_dtor dtor_ctor
         ctor_inject pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms
@@ -2391,8 +2405,8 @@
          #>> apfst massage_res, lthy)
       end;
 
-    fun wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
-      fold_map I wrap_one_etc lthy
+    fun wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types (wrap_one_etcs, lthy) =
+      fold_map I wrap_one_etcs lthy
       |>> apsnd split_list o apfst (apsnd @{split_list 5} o apfst @{split_list 17} o split_list)
         o split_list;
 
@@ -2749,7 +2763,7 @@
           sel_transferss map_o_corec_thmss
       end;
 
-    val lthy'' = lthy'
+    val lthy = lthy
       |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs
       |> @{fold_map 29} define_ctrs_dtrs_for_type_etc fp_bnfs fp_bs fpTs Cs Es ctors dtors
         xtor_co_recs ctor_dtors dtor_ctors ctor_injects pre_map_defs pre_set_defss pre_rel_defs
@@ -2762,7 +2776,7 @@
     val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
       co_prefix fp ^ "datatype"));
   in
-    lthy''
+    lthy
   end;
 
 fun co_datatypes x = define_co_datatypes (K I) (K I) (K I) (K I) x;