tuning

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Oct 02 11:01:20 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Oct 02 12:02:27 2014 +0200
@@ -1832,8 +1832,7 @@
     val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss;
     val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss;
 
-    val fp_eqs =
-      map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs;
+    val fp_eqs = map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs;
 
     val killed_As =
       map_filter (fn (A, set_bos) => if exists is_none set_bos then SOME A else NONE)

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Oct 02 11:01:20 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Oct 02 12:02:27 2014 +0200
@@ -170,8 +170,8 @@
     rel_eqs =
   let
     val ctor_rec_transfers' =
-      map (cterm_instantiate_pos (map SOME passives @ map SOME actives)) ctor_rec_transfers;
-    val ns' = Integer.sum ns;
+      map (cterm_instantiate_pos (map SOME (passives @ actives))) ctor_rec_transfers;
+    val total_n = Integer.sum ns;
   in
     HEADGOAL Goal.conjunction_tac THEN
     EVERY (map (fn ctor_rec_transfer =>
@@ -187,7 +187,7 @@
                  REPEAT_DETERM (HEADGOAL
                    (rtac (mk_rel_funDN 2 case_sum_transfer_eq) ORELSE'
                     rtac (mk_rel_funDN 2 case_sum_transfer))) THEN
-                 HEADGOAL (select_prem_tac ns' (dtac asm_rl) (acc + n)) THEN
+                 HEADGOAL (select_prem_tac total_n (dtac asm_rl) (acc + n)) THEN
                  HEADGOAL (SELECT_GOAL (HEADGOAL
                    ((REPEAT_DETERM o (atac ORELSE'
                        rtac (mk_rel_funDN 1 case_prod_transfer_eq) ORELSE'