1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:11 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:11 2012 +0200
     1.3 @@ -96,11 +96,12 @@
     1.4    EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
     1.5      REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1;
     1.6  
     1.7 -fun mk_induct_prepare_prem_prems_tac 0 = all_tac
     1.8 -  | mk_induct_prepare_prem_prems_tac r =
     1.9 -    REPEAT_DETERM_N r ((rotate_tac ~1) 1 THEN dtac meta_mp 1 THEN
    1.10 -      defer_tac 2 THEN PRIMITIVE (Thm.permute_prems 0 ~1) THEN rotate_tac 1 1) THEN
    1.11 -    PRIMITIVE Raw_Simplifier.norm_hhf;
    1.12 +(* FIXME: why not in "Pure"? *)
    1.13 +fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1);
    1.14 +
    1.15 +fun mk_induct_prepare_prem_prems_tac r =
    1.16 +  REPEAT_DETERM_N r (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2) THEN
    1.17 +  PRIMITIVE Raw_Simplifier.norm_hhf;
    1.18  
    1.19  val induct_prem_prem_thms =
    1.20    @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left
    1.21 @@ -122,7 +123,7 @@
    1.22  (* TODO: Get rid of the "blast_tac" *)
    1.23  fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs =
    1.24    EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
    1.25 -    [select_prem_tac nn (dtac meta_spec) (nn - kk + 1), rotate_tac ~1,(*###*) etac meta_mp,
    1.26 +    [rotate_tac (~ nn), select_prem_tac nn (dtac meta_spec) kk, rotate_tac ~1,(*###*) etac meta_mp,
    1.27       SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), (* ### why on a line of its own? *)
    1.28       SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)),
    1.29       SELECT_GOAL (Local_Defs.unfold_tac ctxt