1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Oct 17 18:53:00 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Oct 17 18:53:00 2013 +0200
     1.3 @@ -88,20 +88,35 @@
     1.4      (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
     1.5    unfold_thms_tac ctxt (@{thm Let_def} :: sel_fs) THEN HEADGOAL (rtac refl);
     1.6  
     1.7 +fun inst_split_eq ctxt split =
     1.8 +  (case prop_of split of
     1.9 +    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) =>
    1.10 +    let
    1.11 +      val s = Name.uu;
    1.12 +      val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
    1.13 +      val split' = Drule.instantiate' [] [SOME (certify ctxt eq)] split;
    1.14 +    in
    1.15 +      Thm.generalize ([], [s]) (Thm.maxidx_of split' + 1) split'
    1.16 +    end
    1.17 +  | _ => split);
    1.18 +
    1.19  (* TODO: reduce code duplication with selector tactic above *)
    1.20  fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =
    1.21 -  HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE'
    1.22 -    Splitter.split_tac (split_if :: splits))) THEN
    1.23 -  mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
    1.24 -  HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
    1.25 -    SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
    1.26 -    (rtac refl ORELSE' atac ORELSE'
    1.27 -     resolve_tac (@{thm Code.abort_def} :: split_connectI) ORELSE'
    1.28 -     Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
    1.29 -     Splitter.split_tac (split_if :: splits) ORELSE'
    1.30 -     mk_primcorec_assumption_tac ctxt discIs ORELSE'
    1.31 -     eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
    1.32 -     (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))));
    1.33 +  let
    1.34 +    val splits' =
    1.35 +      map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits)
    1.36 +  in
    1.37 +    HEADGOAL (REPEAT o (resolve_tac (splits' @ split_connectI))) THEN
    1.38 +    mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
    1.39 +    HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
    1.40 +      SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
    1.41 +      (rtac refl ORELSE' atac ORELSE'
    1.42 +       resolve_tac (@{thm Code.abort_def} :: splits' @ split_connectI) ORELSE'
    1.43 +       Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
    1.44 +       mk_primcorec_assumption_tac ctxt discIs ORELSE'
    1.45 +       eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
    1.46 +       (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))))
    1.47 +  end;
    1.48  
    1.49  fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs =
    1.50    EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) ms