diff -r 3d93e8b4ae02 -r 396999552212 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 01:05:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 01:05:32 2013 +0200
@@ -24,6 +24,10 @@
 open BNF_Util
 open BNF_Tactics
 
+val split_if = @{thm split_if};
+val split_if_asm = @{thm split_if_asm};
+val split_connectI = @{thms allI impI conjI};
+
 fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx =
   unfold_thms_tac ctxt fun_defs THEN
   HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
@@ -60,9 +64,9 @@
   unfold_thms_tac ctxt (@{thms o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN
   HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
     eresolve_tac @{thms not_TrueE FalseE} ORELSE'
-    resolve_tac @{thms allI impI conjI} ORELSE'
-    Splitter.split_asm_tac (@{thm split_if_asm} :: split_asms) ORELSE'
-    Splitter.split_tac (@{thm split_if} :: splits) ORELSE'
+    resolve_tac split_connectI ORELSE'
+    Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
+    Splitter.split_tac (split_if :: splits) ORELSE'
     etac notE THEN' atac));
 
 fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
@@ -70,12 +74,11 @@
     (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
   unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
 
-fun mk_primcorec_code_of_ctr_case_tac ctxt eq_caseIs m f_ctr =
-  HEADGOAL (REPEAT o resolve_tac (@{thm eq_ifI} :: eq_caseIs)) THEN
+fun mk_primcorec_code_of_ctr_case_tac ctxt splits m f_ctr =
+  HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN
   mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
   REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt) THEN
-  (* FIXME: Something like (ss_only @{thms if_True if_False not_False_eq_True simp_thms} ctxt) *)
-  HEADGOAL (asm_simp_tac ctxt);
+  HEADGOAL (rtac refl);
 
 fun mk_primcorec_code_of_ctr_tac ctxt eq_caseIs ms ctr_thms =
   EVERY (map2 (mk_primcorec_code_of_ctr_case_tac ctxt eq_caseIs) ms ctr_thms);