1.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Wed Sep 18 17:36:47 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Wed Sep 18 18:12:40 2013 +0200
     1.3 @@ -134,7 +134,6 @@
     1.4    HEADGOAL (rtac uexhaust THEN'
     1.5      EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));
     1.6  
     1.7 -(* TODO: More precise "simp_thms"; get rid of "blast_tac" *)
     1.8  fun mk_split_tac ctxt uexhaust cases injectss distinctsss =
     1.9    HEADGOAL (rtac uexhaust) THEN
    1.10    ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 18 17:36:47 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 18 18:12:40 2013 +0200
     2.3 @@ -717,7 +717,7 @@
     2.4      (* try to prove (automatically generated) tautologies by ourselves *)
     2.5      val exclss'' = exclss'
     2.6        |> map (map (apsnd
     2.7 -        (`(try (fn t => Goal.prove lthy [] [] t (mk_primcorec_taut_tac lthy |> K))))));
     2.8 +        (`(try (fn t => Goal.prove lthy [] [] t (mk_primcorec_assumption_tac lthy |> K))))));
     2.9      val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss'';
    2.10      val (obligation_idxss, obligationss) = exclss''
    2.11        |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))

     3.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 17:36:47 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 18:12:40 2013 +0200
     3.3 @@ -8,13 +8,13 @@
     3.4  signature BNF_FP_REC_SUGAR_TACTICS =
     3.5  sig
     3.6    val mk_primcorec_code_tac: Proof.context -> thm -> thm list -> tactic
     3.7 -  val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> tactic
     3.8 +  val mk_primcorec_code_of_ctr_tac: Proof.context -> int list -> thm list -> tactic
     3.9    val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
    3.10    val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int ->
    3.11      thm list list list -> thm list -> thm list -> thm list -> tactic
    3.12    val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
    3.13      tactic
    3.14 -  val mk_primcorec_taut_tac: Proof.context -> tactic
    3.15 +  val mk_primcorec_assumption_tac: Proof.context -> tactic
    3.16    val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic
    3.17  end;
    3.18  
    3.19 @@ -30,10 +30,8 @@
    3.20    unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_idents) THEN
    3.21    HEADGOAL (rtac refl);
    3.22  
    3.23 -fun mk_primcorec_taut_tac ctxt =
    3.24 -  HEADGOAL (etac FalseE) ORELSE
    3.25 -  unfold_thms_tac ctxt @{thms de_Morgan_conj de_Morgan_disj not_not not_False_eq_True} THEN
    3.26 -  HEADGOAL (SOLVE o REPEAT o (atac ORELSE' resolve_tac @{thms disjI1 disjI2 conjI TrueI}));
    3.27 +fun mk_primcorec_assumption_tac ctxt =
    3.28 +  HEADGOAL (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt));
    3.29  
    3.30  fun mk_primcorec_same_case_tac m =
    3.31    HEADGOAL (if m = 0 then rtac TrueI
    3.32 @@ -41,7 +39,7 @@
    3.33  
    3.34  fun mk_primcorec_different_case_tac ctxt excl =
    3.35    unfold_thms_tac ctxt @{thms not_not not_False_eq_True} THEN
    3.36 -  HEADGOAL (rtac excl THEN_ALL_NEW SELECT_GOAL (mk_primcorec_taut_tac ctxt));
    3.37 +  HEADGOAL (rtac excl THEN_ALL_NEW SELECT_GOAL (mk_primcorec_assumption_tac ctxt));
    3.38  
    3.39  fun mk_primcorec_cases_tac ctxt k m exclsss =
    3.40    let val n = length exclsss in
    3.41 @@ -67,14 +65,14 @@
    3.42    HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc THEN' REPEAT_DETERM_N m o atac) THEN
    3.43    unfold_thms_tac ctxt sels THEN HEADGOAL (rtac refl);
    3.44  
    3.45 -fun mk_primcorec_code_of_ctr_case_tac ctxt defs ctr_thm =
    3.46 +fun mk_primcorec_code_of_ctr_case_tac ctxt m ctr_thm =
    3.47    HEADGOAL (REPEAT o rtac @{thm eq_ifI}) THEN
    3.48 -  mk_primcorec_prelude ctxt defs (ctr_thm RS trans) THEN
    3.49 -  REPEAT_DETERM_N 2 (HEADGOAL
    3.50 -    (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt)));
    3.51 +  mk_primcorec_prelude ctxt [] (ctr_thm RS trans) THEN
    3.52 +  REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt) THEN
    3.53 +  HEADGOAL (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt));
    3.54  
    3.55 -fun mk_primcorec_code_of_ctr_tac ctxt ctr_thms =
    3.56 -  EVERY (map (mk_primcorec_code_of_ctr_case_tac ctxt []) ctr_thms);
    3.57 +fun mk_primcorec_code_of_ctr_tac ctxt ms ctr_thms =
    3.58 +  EVERY (map2 (mk_primcorec_code_of_ctr_case_tac ctxt) ms ctr_thms);
    3.59  
    3.60  fun mk_primcorec_code_tac ctxt raw collapses =
    3.61    HEADGOAL (rtac (raw RS trans)) THEN unfold_thms_tac ctxt @{thms split_ifs} THEN