--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Tue Sep 24 19:15:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Tue Sep 24 19:54:40 2013 +0200
@@ -78,7 +78,8 @@
HEADGOAL (REPEAT o rtac @{thm eq_ifI}) THEN
mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt) THEN
- HEADGOAL (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt));
+ (* FIXME: Something like (ss_only @{thms if_True if_False not_False_eq_True simp_thms} ctxt) *)
+ HEADGOAL (asm_simp_tac ctxt);
fun mk_primcorec_code_of_ctr_tac ctxt ms ctr_thms =
EVERY (map2 (mk_primcorec_code_of_ctr_case_tac ctxt) ms ctr_thms);