# HG changeset patch
# User blanchet
# Date 1426017196 -3600
# Node ID b3bfbfc92a44b0845e52c6290b91eab691273d96
# Parent  4028c156136a72f9c5ea7cfe4216b2937998fcb5
tuning

diff -r 4028c156136a -r b3bfbfc92a44 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Mar 10 20:12:34 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Mar 10 20:53:16 2015 +0100
@@ -189,12 +189,6 @@
       map (cterm_instantiate_pos (map SOME (passives @ actives))) ctor_rec_transfers;
     val total_n = Integer.sum ns;
     val True = @{term True};
-    fun magic eq xs xs' = Subgoal.FOCUS (fn {prems, ...} =>
-      let
-        val thm = prems
-          |> Ctr_Sugar_Util.permute_like eq xs xs'
-          |> Library.foldl1 (fn (acc, elem) => elem RS (acc RS @{thm rel_funD}))
-      in HEADGOAL (rtac thm) end)
   in
     HEADGOAL Goal.conjunction_tac THEN
     EVERY (map (fn ctor_rec_transfer =>
diff -r 4028c156136a -r b3bfbfc92a44 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 10 20:12:34 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 10 20:53:16 2015 +0100
@@ -155,6 +155,7 @@
 
   val mk_Inl: typ -> term -> term
   val mk_Inr: typ -> term -> term
+  val mk_sumprod_balanced: typ -> int -> int -> term list -> term
   val mk_absumprod: typ -> term -> int -> int -> term list -> term
 
   val dest_sumT: typ -> typ * typ
@@ -414,9 +415,11 @@
 
 val mk_tuple_balanced = mk_tuple1_balanced [];
 
+fun mk_sumprod_balanced T n k ts = Sum_Tree.mk_inj T n k (mk_tuple_balanced ts);
+
 fun mk_absumprod absT abs0 n k ts =
   let val abs = mk_abs absT abs0;
-  in abs $ Sum_Tree.mk_inj (domain_type (fastype_of abs)) n k (mk_tuple_balanced ts) end;
+  in abs $ mk_sumprod_balanced (domain_type (fastype_of abs)) n k ts end;
 
 fun mk_case_sum (f, g) =
   let
diff -r 4028c156136a -r b3bfbfc92a44 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 10 20:12:34 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 10 20:53:16 2015 +0100
@@ -931,7 +931,7 @@
         (build_corec_arg_nested_call ctxt has_call sel_eqns sel)) nested_calls'
     end);
 
-fun build_codefs ctxt bs mxs has_call arg_Tss (corec_specs : corec_spec list)
+fun build_defs ctxt bs mxs has_call arg_Tss (corec_specs : corec_spec list)
     (disc_eqnss : coeqn_data_disc list list) (sel_eqnss : coeqn_data_sel list list) =
   let
     val corecs = map #corec corec_specs;
@@ -1104,7 +1104,7 @@
     val disc_eqnss = @{map 6} mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss
       disc_eqnss0;
     val (defs, excludess') =
-      build_codefs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
+      build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
 
     val tac_opts =
       map (fn {code_rhs_opt, ...} :: _ =>
diff -r 4028c156136a -r b3bfbfc92a44 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Mar 10 20:12:34 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Mar 10 20:53:16 2015 +0100
@@ -539,14 +539,13 @@
 
     val defs = build_defs lthy nonexhaustives bs mxs funs_data rec_specs has_call;
 
-    fun prove def_thms' ({ctr_specs, fp_nesting_map_ident0s, fp_nesting_map_comps, ...}
-        : rec_spec) (fun_data : eqn_data list) lthy' =
+    fun prove def_thms ({ctr_specs, fp_nesting_map_ident0s, fp_nesting_map_comps, ...} : rec_spec)
+        (fun_data : eqn_data list) lthy' =
       let
         val js =
           find_indices (op = o apply2 (fn {fun_name, ctr, ...} => (fun_name, ctr)))
             fun_data eqns_data;
 
-        val def_thms = map (snd o snd) def_thms';
         val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
           |> fst
           |> map_filter (try (fn (x, [y]) =>
@@ -587,7 +586,7 @@
              fun_defs = Morphism.fact phi def_thms, fpTs = take actual_nn Ts};
         in
           map_prod split_list (interpret_lfp_rec_sugar plugins fp_rec_sugar)
-            (@{fold_map 2} (prove defs) (take actual_nn rec_specs) funs_data lthy)
+            (@{fold_map 2} (prove (map (snd o snd) defs)) (take actual_nn rec_specs) funs_data lthy)
         end),
       lthy |> Local_Theory.notes (notes @ common_notes) |> snd)
   end;