1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 22:51:21 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 23:29:49 2013 +0200
     1.3 @@ -1068,7 +1068,7 @@
     1.4                    |> K |> Goal.prove lthy [] [] raw_t;
     1.5  val _ = tracing ("raw code theorem: " ^ Syntax.string_of_term lthy (prop_of raw_code_thm));
     1.6                in
     1.7 -                mk_primcorec_code_of_raw_code_tac lthy sel_splits raw_code_thm
     1.8 +                mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm
     1.9                  |> K |> Goal.prove lthy [] [] t
    1.10  |> tap (tracing o curry (op ^) "code theorem: " o Syntax.string_of_term lthy o prop_of)
    1.11                  |> single

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Sun Oct 20 22:51:21 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Sun Oct 20 23:29:49 2013 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  signature BNF_FP_REC_SUGAR_TACTICS =
     2.5  sig
     2.6    val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic
     2.7 -  val mk_primcorec_code_of_raw_code_tac: Proof.context -> thm list -> thm -> tactic
     2.8 +  val mk_primcorec_code_of_raw_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic
     2.9    val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
    2.10    val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
    2.11      tactic
    2.12 @@ -26,6 +26,7 @@
    2.13  open BNF_Tactics
    2.14  
    2.15  val falseEs = @{thms not_TrueE FalseE};
    2.16 +val Let_def = @{thm Let_def};
    2.17  val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict};
    2.18  val split_if = @{thm split_if};
    2.19  val split_if_asm = @{thm split_if_asm};
    2.20 @@ -86,7 +87,7 @@
    2.21  fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
    2.22    HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'
    2.23      (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
    2.24 -  unfold_thms_tac ctxt (@{thm Let_def} :: sel_fs) THEN HEADGOAL (rtac refl);
    2.25 +  unfold_thms_tac ctxt (Let_def :: sel_fs) THEN HEADGOAL (rtac refl);
    2.26  
    2.27  fun inst_split_eq ctxt split =
    2.28    (case prop_of split of
    2.29 @@ -100,6 +101,9 @@
    2.30      end
    2.31    | _ => split);
    2.32  
    2.33 +fun distinct_in_prems_tac distincts =
    2.34 +  eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
    2.35 +
    2.36  (* TODO: reduce code duplication with selector tactic above *)
    2.37  fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =
    2.38    let
    2.39 @@ -111,10 +115,11 @@
    2.40      HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
    2.41        SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
    2.42        (rtac refl ORELSE' atac ORELSE'
    2.43 -       resolve_tac (@{thm Code.abort_def} :: splits' @ split_connectI) ORELSE'
    2.44 +       resolve_tac (@{thm Code.abort_def} :: split_connectI) ORELSE'
    2.45 +       Splitter.split_tac (split_if :: splits) ORELSE'
    2.46         Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
    2.47         mk_primcorec_assumption_tac ctxt discIs ORELSE'
    2.48 -       eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
    2.49 +       distinct_in_prems_tac distincts ORELSE'
    2.50         (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))))
    2.51    end;
    2.52  
    2.53 @@ -124,13 +129,14 @@
    2.54    IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
    2.55      HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)));
    2.56  
    2.57 -fun mk_primcorec_code_of_raw_code_tac ctxt splits raw =
    2.58 +fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw =
    2.59    HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'
    2.60 -    SELECT_GOAL (unfold_thms_tac ctxt @{thms Let_def}) THEN' REPEAT_DETERM o
    2.61 -    (rtac refl ORELSE'
    2.62 -     (TRY o rtac sym) THEN' atac ORELSE'
    2.63 +    SELECT_GOAL (unfold_thms_tac ctxt [Let_def]) THEN' REPEAT_DETERM o
    2.64 +    (rtac refl ORELSE' atac ORELSE'
    2.65       resolve_tac split_connectI ORELSE'
    2.66       Splitter.split_tac (split_if :: splits) ORELSE'
    2.67 +     distinct_in_prems_tac distincts ORELSE'
    2.68 +     rtac sym THEN' atac ORELSE'
    2.69       etac notE THEN' atac));
    2.70  
    2.71  end;