# HG changeset patch
# User blanchet
# Date 1473149373 -7200
# Node ID 362160f9c68a2bc171110ba27316acfd63f89146
# Parent  dbda3556d495e068e073f4a6e23ecf42f0c626e1
tuned ML signature

diff -r dbda3556d495 -r 362160f9c68a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 05 20:57:07 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 06 10:09:33 2016 +0200
@@ -2162,8 +2162,6 @@
         warn (order_strong_conn (op =) Int_Graph.make Int_Graph.topological_order deps sccs)
       end;
 
-    val fp_eqs = map dest_TFree Xs ~~ ctrXs_repTs;
-
     val killed_As =
       map_filter (fn (A, set_bos) => if exists is_none set_bos then SOME A else NONE)
         (As ~~ transpose set_boss);
@@ -2174,8 +2172,8 @@
              xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts,
              xtor_co_rec_transfers, xtor_co_rec_o_maps, ...},
            lthy)) =
-      fixpoint_bnf I (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs
-        (map dest_TFree As) (map dest_TFree killed_As) fp_eqs empty_comp_cache no_defs_lthy
+      fixpoint_bnf I (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs (map dest_TFree As)
+        (map dest_TFree killed_As) (map dest_TFree Xs) ctrXs_repTs empty_comp_cache no_defs_lthy
       handle BAD_DEAD (X, X_backdrop) =>
         (case X_backdrop of
           Type (bad_tc, _) =>
diff -r dbda3556d495 -r 362160f9c68a src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 05 20:57:07 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Sep 06 10:09:33 2016 +0200
@@ -109,8 +109,8 @@
       case f x of SOME y => (y :: ys, (x :: good, bad)) | NONE => (ys, (good, x :: bad)))
     xs ([], ([], []));
 
-fun key_of_fp_eqs fp As fpTs fp_eqs =
-  Type (case_fp fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs)
+fun key_of_fp_eqs fp As fpTs Xs ctrXs_repTs =
+  Type (case_fp fp "l" "g", fpTs @ Xs @ ctrXs_repTs)
   |> Term.map_atyps (fn T as TFree (_, S) =>
     (case find_index (curry (op =) T) As of
       ~1 => T
@@ -212,8 +212,7 @@
     val kss = map (fn n => 1 upto n) ns;
     val mss = map (map length) ctr_Tsss;
 
-    val fp_eqs = map dest_TFree Xs ~~ ctrXs_repTs;
-    val key = key_of_fp_eqs fp As fpTs fp_eqs;
+    val key = key_of_fp_eqs fp As fpTs Xs ctrXs_repTs;
   in
     (case n2m_sugar_of no_defs_lthy key of
       SOME n2m_sugar => (n2m_sugar, no_defs_lthy)
@@ -242,7 +241,7 @@
         val (((pre_bnfs, absT_infos), _), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
                dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
           fixpoint_bnf I (construct_mutualized_fp fp mutual_cliques fpTs indexed_fp_ress)
-            fp_bs As' killed_As' fp_eqs empty_comp_cache no_defs_lthy;
+            fp_bs As' killed_As' (map dest_TFree Xs) ctrXs_repTs empty_comp_cache no_defs_lthy;
 
         val time = time lthy;
         val timer = time (Timer.startRealTimer ());
diff -r dbda3556d495 -r 362160f9c68a src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Sep 05 20:57:07 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Sep 06 10:09:33 2016 +0200
@@ -209,8 +209,8 @@
   val fixpoint_bnf: (binding -> binding) ->
       (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
       BNF_Comp.absT_info list -> local_theory -> 'a) ->
-    binding list -> (string * sort) list -> (string * sort) list -> ((string * sort) * typ) list ->
-    BNF_Comp.comp_cache -> local_theory ->
+    binding list -> (string * sort) list -> (string * sort) list -> (string * sort) list ->
+    typ list -> BNF_Comp.comp_cache -> local_theory ->
     ((BNF_Def.bnf list * BNF_Comp.absT_info list) * BNF_Comp.comp_cache) * 'a
   val fp_antiquote_setup: binding -> theory -> theory
 end;
@@ -925,13 +925,12 @@
     #> extra_qualify #> Binding.concealed
   end;
 
-fun fixpoint_bnf extra_qualify construct_fp bs resBs Ds0 fp_eqs comp_cache0 lthy =
+fun fixpoint_bnf extra_qualify construct_fp bs resBs Ds0 Xs rhsXs comp_cache0 lthy =
   let
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
 
-    val nn = length fp_eqs;
-    val (Xs, rhsXs) = split_list fp_eqs;
+    val nn = length Xs;
 
     fun flatten_tyargs Ass =
       subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
diff -r dbda3556d495 -r 362160f9c68a src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Sep 05 20:57:07 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Tue Sep 06 10:09:33 2016 +0200
@@ -405,7 +405,7 @@
 
 fun mk_nth_conv n m =
   let
-    fun thm b = if b then @{thm fstI} else @{thm sndI}
+    fun thm b = if b then @{thm fstI} else @{thm sndI};
     fun mk_nth_conv _ 1 1 = refl
       | mk_nth_conv _ _ 1 = @{thm fst_conv}
       | mk_nth_conv _ 2 2 = @{thm snd_conv}