# HG changeset patch
# User blanchet
# Date 1367226296 -7200
# Node ID d4c1abbb4095c04fbff868597ef7c4635a234fc1
# Parent  355dcd6a9b3cb70bde7f98d3163bc507459a08fc
code tuning

diff -r 355dcd6a9b3c -r d4c1abbb4095 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Apr 29 10:37:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Apr 29 11:04:56 2013 +0200
@@ -7,6 +7,10 @@
 
 signature BNF_CTR_SUGAR =
 sig
+  type ctr_wrap_result =
+    term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
+    thm list list
+
   val rep_compat_prefix: string
 
   val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
@@ -21,8 +25,7 @@
   val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     (((bool * bool) * term list) * term) *
       (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
-    (term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
-     thm list list) * local_theory
+    ctr_wrap_result * local_theory
   val parse_wrap_options: (bool * bool) parser
   val parse_bound_term: (binding * string) parser
 end;
@@ -33,6 +36,10 @@
 open BNF_Util
 open BNF_Ctr_Sugar_Tactics
 
+type ctr_wrap_result =
+  term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
+  thm list list;
+
 val rep_compat_prefix = "new";
 
 val isN = "is_";
@@ -309,7 +316,7 @@
 
           val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
             no_defs_lthy
-            |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr => fn b =>
+            |> apfst split_list o fold_map3 (fn k => fn exist_xs_u_eq_ctr => fn b =>
                 if Binding.is_empty b then
                   if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
                   else pair (alternate_disc k, alternate_disc_no_def)
@@ -318,7 +325,7 @@
                 else
                   Specification.definition (SOME (b, NONE, NoSyn),
                     ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
-              ks ms exist_xs_u_eq_ctrs disc_bindings
+              ks exist_xs_u_eq_ctrs disc_bindings
             ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
               Specification.definition (SOME (b, NONE, NoSyn),
                 ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos