1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 02:25:33 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 02:34:34 2013 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4  open BNF_Util
     1.5  open BNF_Tactics
     1.6  
     1.7 +val falseEs = @{thms not_TrueE FalseE};
     1.8  val split_if = @{thm split_if};
     1.9  val split_if_asm = @{thm split_if_asm};
    1.10  val split_connectI = @{thms allI impI conjI};
    1.11 @@ -68,7 +69,7 @@
    1.12    mk_primcorec_cases_tac ctxt k m exclsss THEN
    1.13    unfold_thms_tac ctxt (@{thms o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN
    1.14    HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
    1.15 -    eresolve_tac @{thms not_TrueE FalseE} ORELSE'
    1.16 +    eresolve_tac falseEs ORELSE'
    1.17      resolve_tac split_connectI ORELSE'
    1.18      Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
    1.19      Splitter.split_tac (split_if :: splits) ORELSE'
    1.20 @@ -79,25 +80,22 @@
    1.21      (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
    1.22    unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
    1.23  
    1.24 -fun mk_primcorec_split distincts discIs collapses splits split_asms =
    1.25 +fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits split_asms m f_ctr =
    1.26 +  HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN
    1.27 +  mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
    1.28 +  REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt discIs) THEN
    1.29    HEADGOAL (SELECT_GOAL (HEADGOAL (REPEAT_DETERM o
    1.30      (rtac refl ORELSE' atac ORELSE'
    1.31 -     eresolve_tac (@{thms not_TrueE FalseE} @ map (fn thm => thm RS trans) collapses) ORELSE'
    1.32 +     eresolve_tac (falseEs @ map (fn thm => thm RS trans) collapses) ORELSE'
    1.33       resolve_tac split_connectI ORELSE'
    1.34       Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
    1.35       Splitter.split_tac (split_if :: splits) ORELSE'
    1.36       eresolve_tac (map (fn thm => thm RS @{thm neq_eq_eq_contradict}) distincts) THEN' atac ORELSE'
    1.37       (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac))));
    1.38  
    1.39 -fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits split_asms m f_ctr =
    1.40 -  HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN
    1.41 -  mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
    1.42 -  REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt discIs) THEN
    1.43 -  mk_primcorec_split distincts discIs collapses splits split_asms;
    1.44 -
    1.45 -fun mk_primcorec_code_of_ctr_tac ctxt distincs discIs collapses splits split_asms ms ctr_thms =
    1.46 -  EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincs discIs collapses splits split_asms)
    1.47 -    ms ctr_thms);
    1.48 +fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs collapses splits split_asms ms ctr_thms =
    1.49 +  EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits
    1.50 +    split_asms) ms ctr_thms);
    1.51  
    1.52  fun mk_primcorec_code_of_raw_tac splits disc_excludes raw collapses =
    1.53    HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o