# HG changeset patch # User blanchet # Date 1412244147 -7200 # Node ID ce0b9be06f85b41647fa66df5f6ec87b294c1cc7 # Parent 11c6525441086f2e20ee6998c8567d1672e8359e tuning diff -r 11c652544108 -r ce0b9be06f85 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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) diff -r 11c652544108 -r ce0b9be06f85 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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'